Propositional Formula Simplification:  An Exploration Tool

By Vanessa Clark

For a recent CSE545 (Automated Theorem Proving) project, I wrote a program that allows the user to explore the simplification of a propositional formula.

Inputs:  a propositional formula in DIMACS CNF format

                a sequence of decisions (assigning T or F to variables in the formula, i.e. v1=F, v7=T, v2=T)

Output: an HTML file displaying all clauses of the formula, showing their simplifications after each input decision is made.  All unit propagations (colored in blue) are carried out at each step.  The HTML file also mentions whether the formula is satisfied, not satisfied, or neither.  The step where this happens has the clauses colored in green (satisfied) or red (not satisfied).

Examples:

Simple satisfied formula, with unit propagation (in blue):

java CNFDecisionTree cnfinput1.txt outputdemo1.html v1=T v2=F

With input cnfinput1.txt and decisions v1=T, v2=F, the program gives HTML output outputdemo1.html

Simple unsatisfied formula, with unit propagation:

java CNFDecisionTree cnfinput3.txt outputdemo2.html v3=F

Simple formula, neither satisfied nor unsatisfied, without unit propagation necessary, on a larger scale:

java CNFDecisionTree cnfinput2.txt outputdemo3.html v9=F v5=F v16=F v20=T

Large-scale example, with no decisions and only unit propagations:

java CNFDecisionTree test.cnf outputdemo6.html

Large-scale example, with decisions.  Despite the large number of clauses and variables, the program computes this quickly (in about 12 seconds), but the output file is a very large file, so it is not included here.  You can try it on your own, but don't attempt to open it or click on it unless you are prepared to wait.

java CNFDecisionTree test.cnf outputdemo7Large.html v598=T v4=T v63=T v17=F v499=T

Download

This was implemented in Java.  To get the code, check out this ZIP file. 

Instructions:

 - Unzip the file into a directory

 - You shouldn't have to recompile, but if you want to, type "javac *.java"

 - To run the program, type at the command prompt while in the directory you just unzipped:  "java CNFDecisionTree inputCNFfilename outputHTMLfilename decisionList", where inputCNFfilename and outputHTMLfilename are in the current directory, and decisionList is in the form "v1=T v5=F v100=F v3=T" (it also can be omitted).  For examples, try the ones mentioned above or use demo1.bat through demo7.bat or test1.bat through test8.bat.  *Note: You must have Java installed to use this.

For the initial project proposal, including an outline of the implementation approach, click here.

Back to Vanessa's Computer Science labs   ~   Vanessa's homepage