# SAT Simplification

A CNF cleanup tool

Original 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

akabeko (2017-09-02-15-06-59-253)

Hi, I am trying to work out how to remove duplicate elements in a list of lists in prolog.

E.g. input: [[1,2,3],[5,6],[3,4],[1,7]]

Expected output: [[1,2,3],[5,6],[4],[7]]

I know I can use the method sort/2 to remove duplicates in a single list, but how do I get it to work across multiple lists?

``````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.

kk (2013-10-01-12-54-59-044)

those