A CNF cleanup tool

Original A CNF cleanup tool Editable
version 1 of 1



Often I'll be trying to make a new sort of generalized SAT pattern. Usually this consists of a combination of brute-force enumeration and logical deduction, with a smattering of test cases on the corners.

One helpful tool consumes a verbose brute force CNF and returns a more minimal expression without redundancy. Patterns become much more visible after such a cleanup, helped along by pretty-printing the CNF in tidy columns.

BE AWARE: Every sat solver already does this step internally and much much faster. There is no reason to use this code in the solving pipeline - it is for exploration and experimentation.

source at github, simplify.py

Simplification methods

Remove duplicate clauses. If it was correct the first time, it'll still be correct later.

Remove tautologies. For example, anything with A -A in it will always evaluate to true. Regardless of what else is in the clause.

 

Remove terms that cancel out. If there are two clauses

Hi, I am trying to work out how to remove duplicate elements in a ...


 

A B
A -B

then the possible answers are (A=true, B=true) and (A=true, B=false).
B has no effect and the two clauses can be collapsed to simply

A

Remove perfect supersets. In the case of

A B C
A B

the state of C has no effect. The entire A B C clause can be safely eliminated.

 

These are the most basic simplification processes. Various papers describe more advanced transformations, but these are beyond me for now.

those