[Haskell-cafe] Sat solver

[Ron de Bruijn]

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
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Sat solver

[Josef Svenningsson]

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
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe