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

--KW 8-)

```