RSS
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.
A CNF cleanup tool
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
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
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?