Program 3, CS 463
Due at the beginning of class on Wednesday, Oct. 10th.
This assignment uses several heuristic search techniques to find possibly optimal
truth assignments for variables in Boolean formulas.
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 four techniques:
- a genetic algorithm;
- hill climbing, also known as local search;
- constraint solving with forward search;
- the DPLL algorithm;
- the WalkSAT algorithm;
- resolution.
To do:
Run each of your three algorithms on each formula. If your algorithm uses randomness, do 10 runs per formula. Collect data, for each formula and each run, on the time taken, and the highest value of c found. Put these data in tables or graphs (clearly labeled!)
To hand in:
On paper:
- A brief description of each algorithm, including design decisions (how you set your parameters in the genetic algorithm, for instance);
- the data you collected;
- a brief statement of what you learned.
Email your code to Dr. Goldsmith
You will find a huge set of CNF formulas, and a README, in this directory. You should also use the 10 formulas in
this directory.