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