Assignment 2a: Finding the phase transition (BDD)
Issued 3 March; Handin 09.00, 14 March
Introduction
In this assignment you will gain some
familiarity with a SAT package and experiment with this package.
Tasks
- Write an ML program to create random DIMACS format CNF problems by repeatedly generating and conjoining random 3-SAT clauses, using a given number N of variables.
- Use a SAT solver to find whether example is satisfiable. Instrument your program to collect data on the time taken to solve each example. Experiment with various numbers of variables and clause/variable ratios.
- Use your results to plot an experimental phase transition graph, for various numbers of variables.
Instructions
Either find a SAT package on the net, or use one of the following on a DICE machine.
-
/home/mfourman/bin/BerkMin561 Run the program without any command-line arguments to get instructions.
-
/home/mfourman/bin/sp-1.4/sp
Try sp -h for help, or see /home/mfourman/bin/sp-1.4/README for instructions.
Hints
The Unix utility
time will allow you to time execution of a program.
Author: Michael Fourman
Revision 1.1 by
neilb
2004/08/09 22:04:03
