[Haskell-cafe] 2-CNF Sat algorithm/haskell code

[Keith Wansbrough]

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

--KW 8-)