6.825: Techniques in Artificial Intelligence
Fall, 2002

Project 1, Part B: Tools

zChaff

zChaff is a very efficient implementation of the complete SAT solver, Chaff. zChaff takes sentences in CNF form and produces an assignment, if one exists.
More information about zChaff can be found at the zChaff homepage.
Information on the standard DIMACS CNF format can be found here. Here is one example of a CNF sentence in the DIMACS format, and here is another example.

To get zChaff, dowload one of the following files:

	Instructions	Tested On
zChaff binary for Linux	Download the gzipped file Execute: gunzip zchaff.2001.2.17.linux.gz Execute: chmod +x zchaff.2001.2.17.linux To Run: ./zchaff.2001.2.17.linux test1.dimacs	RedHat Linux 6.2, Debian GNU/Linux 2.4.9, Mandrake 8.0
zChaff binary for Solaris	Download the gzipped file Execute: gunzip zchaff.2001.2.17.solaris.gz Execute: chmod +x zchaff.2001.2.17.solaris To Run: ./zchaff.2001.2.17.solaris test1.dimacs	Athena
zChaff C++ source code	Download the gzipped tar file Execute: gunzip zchaff.2001.2.17.src.tar.gz Execute: tar -xvf zchaff.2001.2.17.src.tar Execute: make or make TARGET To Run: ./asap test1.dimacs	Compiles and runs on Debian GNU/Linux 2.4.9 and Mandrake 8.0, but not on RedHat 6.2. Requires libstdc++-libc6.1-2.so.3

What remains is to turn sentences in our CNF format into DIMACS format, and to turn zChaff's assignments into Interpretations for the original sentences.
We have written routines to do the two conversions as part of the techniques.PL.CNF class.

Here is how you can use the routines:

In your program, convert the CNF sentence into a DIMACS-format sentence, and record the mapping of CNF variable names to DIMACS variable names:

CNF.pl2dimacs( CnfFilenameString ); // creates two files: "CnfFilenameString.dimacs" and "CnfFilenameString.dimacs.map"
CNF.pl2dimacs( CnfFilenameString, DimacsFilneameString ); // creates two files: "DimacsFilneameString" and "DimacsFilneameString.map"
CNF.pl2dimacs( CnfSentence, DimacsFilenameString ); // creates two files: "DimacsFilneameString" and "DimacsFilneameString.map"

At the command line (or with a system call), run zChaff on the DIMACS file

zchaff.2001.2.17.solarismysentence.dimacs >! mysentence.zchaff

In your program, convert the zChaff output into an Interpretation for the original CNF sentence. Note that the Interpretation will be null if zChaff did not find an assignment.

Interpretation interp = CNF.zchaffToInterpretation( "mysentence.zchaff","mysentence.dimacs.map");