2SAT in C

[djhulme]

Hi,

Does anyone have a good implementation of 2SAT in C they could give
me?

I can get hold of loads of algorithms, but I'm just being lazy and
don't want to code something up that someone has already done -
probably better than I ever could.

For instance, does anyone have an implementation of BinSAT:

http://www.ii.uam.es/~delval/ps/aaai00a-2sat.pdf

Kind regards,

Daniel

 

[user923005]

Hi,

Does anyone have a good implementation of 2SAT in C they could give
me?

I can get hold of loads of algorithms, but I'm just being lazy and
don't want to code something up that someone has already done -
probably better than I ever could.

For instance, does anyone have an implementation of BinSAT:

http://www.ii.uam.es/~delval/ps/aaai00a-2sat.pdf

Too lazy for a web search too, apparently. This:
http://www.google.com/search?hl=en&q=2SAT+in+C
gives 580,000 hits.

This isn't comp.sources.wanted, which is a waste of time anyway. Just
do a web search or try sourceforge for things like this.

FCOL.

 

[tchow]

Too lazy for a web search too, apparently. This:
http://www.google.com/search?hl=en&q=2SAT+in+C
gives 580,000 hits.

And that's supposed to be helpful? I haven't finished checking all 580,000
hits (perhaps you have?), but the first 20 weren't helpful.

This isn't comp.sources.wanted, which is a waste of time anyway. Just
do a web search or try sourceforge for things like this.

Sourceforge is usually a good pointer, but it's not so easy to answer this
particular request on there.

My suggestion to the original requestor is that, if all you want is to have
someone else do your coding for you, just use MiniSAT or SatELite, which has
done very well in recent SAT solver contests.

http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/

This isn't specific to 2-SAT, but it can handle 2-SAT, and will probably be
plenty fast for most purposes.

 

[Mark McIntyre]

And that's supposed to be helpful?

Yes.

I haven't finished checking all 580,000
hits (perhaps you have?), but the first 20 weren't helpful.

So what? The good folks in comp.lang.c can't answer every blasted
question that comes along, whether remotely related to C or not.
Eventually people need to do their own research.
--
Mark McIntyre

"Debugging is twice as hard as writing the code in the first place.
Therefore, if you write the code as cleverly as possible, you are,
by definition, not smart enough to debug it."
--Brian Kernighan

 

[user923005]

And that's supposed to be helpful? I haven't finished checking all 580,000
hits (perhaps you have?), but the first 20 weren't helpful.

I expect that the OP is smart enough to add additional filtering
criteria to narrow down to what he/she is specifically looking for.

Sourceforge is usually a good pointer, but it's not so easy to answer this
particular request on there.

My suggestion to the original requestor is that, if all you want is to have
someone else do your coding for you, just use MiniSAT or SatELite, which has
done very well in recent SAT solver contests.

http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/

This isn't specific to 2-SAT, but it can handle 2-SAT, and will probably be
plenty fast for most purposes.

My suggestion to the OP is:
1. Look for preexising solutions (what he is doing now, which is a
very intelligent idea, but he is looking in the *wrong* place).
2. Code it himself.
OR
3. Hire someone to code it.

 

[djhulme]

I expect that the OP is smart enough to add additional filtering

criteria to narrow down to what he/she is specifically looking for.

Thanks.

No, I'm not stupid - I build SAT-solvers for my PhD. However my
implementation of 2SAT is pretty lame; and given that I've spent 2
weeks trying to find a good implementation I decided that it might be
wise to ask the comp.lang.c and comp.theory groups, since I suspect a
large majority of Theoretical Computer Scientists (such as myself)
have implemented 2SAT algorithms in a much better way than I ever
could.

Indeed. Tried there also.

Thanks for this. I'm familiar with the SAT community - it's really a
fast implementation of 2SAT I'm interested in. If i can't find a good
one, then I'll have to implement my version in hardware i suspect.

My suggestion to the OP is:
1. Look for preexising solutions (what he is doing now, which is a
very intelligent idea, but he is looking in the *wrong* place).

That's why i posted to comp.lang.c and comp.thoery

2. Code it himself.

Tried that - I'm not the worlds best coder, and don't really have time
to reinvent the wheel.

OR
3. Hire someone to code it.

I might have to do this, but it kind of defeats the object.

Thanks once again to the people who gave constructive comments.

Daniel

 

[Richard]

I expect that the OP is smart enough to add additional filtering
criteria to narrow down to what he/she is specifically looking for.


My suggestion to the OP is:
1. Look for preexising solutions (what he is doing now, which is a
very intelligent idea, but he is looking in the *wrong* place).
2. Code it himself.
OR
3. Hire someone to code it.

Pretty wide ranging "suggestions".

You forgot "design it himself" or "pay someone to design it".

I think your original "try google" was more helpful ......

 

[tchow]

Thanks for this. I'm familiar with the SAT community - it's really a
fast implementation of 2SAT I'm interested in. If i can't find a good
one, then I'll have to implement my version in hardware i suspect.

What is it about your application that precludes a fast general SAT solver
as opposed to a specialized 2SAT solver?

The usual proof that 2SAT is solvable in polynomial time proceeds by
demonstrating that resolution gives you a polytime algorithm. Although
I haven't studied 2SAT solving in any detail, I suspect that a lot of
the ideas for sleekening a 2SAT solver will be very similar to the ideas
for sleekening a general resolution-based SAT solver. Since so much
more effort has been expended on developing general SAT solvers, there's
a good chance that as far as ready-made software goes, the general SAT
solvers will run faster on 2SAT problems than special-purpose 2SAT solvers.

 

[user923005]

Thanks.

No, I'm not stupid - I build SAT-solvers for my PhD. However my
implementation of 2SAT is pretty lame; and given that I've spent 2
weeks trying to find a good implementation I decided that it might be
wise to ask the comp.lang.c and comp.theory groups, since I suspect a
large majority of Theoretical Computer Scientists (such as myself)
have implemented 2SAT algorithms in a much better way than I ever
could.


Indeed. Tried there also.


Thanks for this. I'm familiar with the SAT community - it's really a
fast implementation of 2SAT I'm interested in. If i can't find a good
one, then I'll have to implement my version in hardware i suspect.


That's why i posted to comp.lang.c and comp.thoery


Tried that - I'm not the worlds best coder, and don't really have time
to reinvent the wheel.


I might have to do this, but it kind of defeats the object.

Thanks once again to the people who gave constructive comments.

You might try
Perhaps this link is helpful:
http://www.lri.fr/~simon/contest/results/