[Haskell-cafe] 2-CNF Sat algorithm/haskell code
Keith.Wansbrough at cl.cam.ac.uk
Wed Mar 17 10:59:04 EST 2004
> Dear Haskellers,
> Today I searched over more than an hour on the web to
> find an implementation of an algorithm that was first
> written in the 1970's that solves 2-Conjuntive Normal
> Form logical sentences in polynomial time.
I don't recall the exact algorithm, but here are some observations:
- a 2CNF clause (x \/ y) is a pair of implications
( -x => y /\ -y => x).
- if there are n variables, the graph used has 2n nodes, one for each
literal (for a variable x, there is a node x and a node -x).
- add edges for each implication arising from a clause.
- observe that for each path x => y => z => w there is an antipath
-w => -z => -y => -x.
- observe that as long as there is no cycle containing a literal and
its negation, the problem is solvable.
- observe that (if the problem is solvable) you can remove a terminal
edge by asserting the terminal literal (dually, you can remove an
initial edge by asserting the negation of the initial literal).
- so I guess you can keep going until there's nothing left; if you
have a cycle left, then arbitrarily set or clear all its literals;
if you can't, the problem is insoluble.
I haven't proved this, but it made sense to me when I thought about it
a couple of weeks ago.
More information about the Haskell-Cafe