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. The only thing I could find were some homework assignments for students of universities and I learned that there exist an algoritm for 2-CNF. Although I am a student, what I am doing is no homework. I believe the datastructure used was a strongly connected graph (perhaps this rings any bells). If you don't know any implementation in any imperative language or functional language (not to far off when compared to Haskell), a clear pseudo-code description, either written by yourself or a URL to a webpage/paper with that information would also be very welcome. Thanks in advance, Ron de Bruijn P.S. This is really offtopic, but I would like to hear some opinions about this project: http://www.supercompilers.com/ I don't know whether they are for real, but when this works it would greatly impacts the use of inefficient functional programs(when applied to it ofcourse). Like in Haskell, a lot of programs could be written like: [x|x<-someList, somePred x] Although they computationally seen would be very slow, without "supercompilation", with they would perform just as good as some smart way of doing it. __________________________________ Do you Yahoo!? Yahoo! Mail - More reliable, more storage, less spam http://mail.yahoo.com
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-)
participants (2)
-
Keith Wansbrough -
Ron de Bruijn