COMP316A, 2012 Assignment III

COMP316A. 2012 Artificial Intelligence Techniques and Applications

Assignment 3 - Solving 3SAT

This assignment is due by Monday May 7th at 11.55pm. 

This assignment accounts for 1/6 of your internal 316 marks. 

----------------------------------------------------------------------

Question 1 (50 marks): Testing WalkSAT

----------------------------------------------------------------------

Implement the WalkSAT algorithm (see book or lecture slides).

Use p = 0.5 for all experiments. Set MAXFLIPS to 10^9
Generate random solvable 3SAT problems with 100 propositional
variables. Generate problems with 100, 200, 300, ... 1000
clauses, i.e. have a ratios of clauses/variables from 1 up to 10.
For each problem size generate 5 random problems, use WalkSAT
to solve them, and record the number of flips needed.

Prepare a result table: ratio x run -> number of flips
 
             run 1   run 2   run 3   run 4   run 5  median
ratio = 1   123456  456722  956722  246801  367489  367489
ratio = 2  ...
...

How to generate random solvable problems:

1) generate a random truth value assignment for the 100 variables
2) generate as many random clauses as needed (between 100 and 1000):
   to generate one random clause consisting of three disjuncts:
    a) draw three variables out of the 100 at random (avoid duplicates!)
    b) draw one of the three at random: if it is true, use it as is,
         if it is false, add its negation to your clause
    c) for the remaining two variables select at random, whether to
       include the variable as is or negated.

What to hand in: source code + result table

----------------------------------------------------------------------

Question 2 (50 marks): Testing DPLL

----------------------------------------------------------------------

Implement the DPLL algorithm (see book or lecture slides).

Run it on the exact same random 3SAT problems that you
were using to test WalkSAT. You may terminate runs that
take excessive time. 

Prepare a result table: ratio x run -> [ DPLL runtime / WalkSAT runtime ]
 
             run 1   run 2   run 3   run 4   run 5  median
ratio = 1      5.1     3.7      4.8    DNF     5.7    4.95  
ratio = 2  ...
...

What to hand in: source code + result table

----------------------------------------------------------------------

Again, you may use any of the following languages: Java, C, C++, C#, Python, Ruby, Haskell.