Hi there, I need a complete 3-CNF-Sat solver that can solve sentences of about length 20 (or shorter). Now I use simple model checking, but that's a bit slow , you understand :) I have seen some algorithms on the web and some code-sniplets in papers. But I presume there is some implementation available, so I thought: Let's ask, and don't reinvent the wheel. Greets Ron P.S. Thanks to those who answered my previous question, although I have found another way of expressing my problem. __________________________________ Do you Yahoo!? Yahoo! Finance: Get your refund fast by filing online. http://taxes.yahoo.com/filing.html
Hi, On Thu, 5 Feb 2004, Ron de Bruijn wrote:
Hi there,
I need a complete 3-CNF-Sat solver that can solve sentences of about length 20 (or shorter).
Now I use simple model checking, but that's a bit slow , you understand :)
I have seen some algorithms on the web and some code-sniplets in papers. But I presume there is some implementation available, so I thought: Let's ask, and don't reinvent the wheel.
Well, I don't know a any good sat solver written in haskell. But there are plenty written in c/c++. One example is Satzoo which is pretty good: http://www.cs.chalmers.se/~een/Satzoo/ I have a haskell binding to Satzoo if you're interested. Just mail me. HTH, /Josef
participants (2)
-
Josef Svenningsson -
Ron de Bruijn