Program 3: SAT Assignment
This assignment uses several heuristic search techniques to find possibly optimal truth assignments for variables in the given Boolean formulas (see the bottom of the assignment).
The formulas are in conjunctive normal form (ANDs of ORs). The fitness of an assignment is the number of clauses (ORs) that the assignment satisfies. If there are c clauses, then the highest fitness is bounded by c. However, if the formula is not satisfiable, then you cannot simultaneously make all c clauses
true.
You will use three of the following seven techniques:
1. DPLL
2. Resolution
3. Genetic algorithms
4. Local search
5. Simulatedannealing
6. GSAT
7. WalkSAT
You must choose at least one complete algorithm to implement – DPLL or
Resolution.
To do:
Run each of your three algorithms on each formula. If your algorithm uses randomness (genetic algorithm, simulated annealing, GSAT, WalkSAT), do 10 runs per formula. Collect data, for each formula and each run, on the time taken, and the highest value of c (highest number of satisfied clauses for any assignment) found. Put these data in tables or graphs (clearly labeled!) (How long did it take as a function of number of clauses satisfied, or perhaps
formula number vs. time.)
To hand in:
• A brief description of each algorithm, including design decisions (how you
set your parameters in the genetic algorithm, for instance)
• Your code
• The data you collected (graphs!)
• A learning outcome section
You can find information about the format for the formulas here (Links to an external site.). (Links to an external site.)
You will use the formulas in the directory you will find under Files (see Canvas sidebar).