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, download one of the following files:

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:

1. 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"
   
   
2. At the command line (or with a system call), run zChaff on the DIMACS file
   
   • zchaff.2001.2.17.solaris mysentence.dimacs >! mysentence.zchaff
   
   
3. 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");