By using this site, you agree to our updated Privacy Policy and our Terms of Use. Manage your Cookies Settings.
455,902 Members | 1,245 Online
Bytes IT Community
+ Ask a Question
Need help? Post your question and get tips & solutions from a community of 455,902 IT Pros & Developers. It's quick & easy.

2SAT in C

P: n/a
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

May 30 '07 #1
Share this Question
Share on Google+
8 Replies


P: n/a
On May 30, 3:47 am, djhu...@gmail.com wrote:
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.
May 30 '07 #2

P: n/a
In article <11*********************@p47g2000hsd.googlegroups. com>,
user923005 <dc*****@connx.comwrote:
>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/Researc...thods/MiniSat/

This isn't specific to 2-SAT, but it can handle 2-SAT, and will probably be
plenty fast for most purposes.
--
Tim Chow tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences
May 30 '07 #3

P: n/a
On 30 May 2007 22:18:14 GMT, in comp.lang.c , tc***@lsa.umich.edu
wrote:
>In article <11*********************@p47g2000hsd.googlegroups. com>,
user923005 <dc*****@connx.comwrote:
>>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?
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
May 30 '07 #4

P: n/a
On May 30, 3:18 pm, t...@lsa.umich.edu wrote:
In article <1180553658.423749.84...@p47g2000hsd.googlegroups. com>,

user923005 <dcor...@connx.comwrote:
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.
I expect that the OP is smart enough to add additional filtering
criteria to narrow down to what he/she is specifically looking for.
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/Researc...thods/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.

May 30 '07 #5

P: n/a
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.
Sourceforge is usually a good pointer, but it's not so easy to answer this
particular request on there.
Indeed. Tried there also.
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/Researc...thods/MiniSat/
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

May 31 '07 #6

P: n/a
user923005 <dc*****@connx.comwrites:
On May 30, 3:18 pm, t...@lsa.umich.edu wrote:
>In article <1180553658.423749.84...@p47g2000hsd.googlegroups. com>,

user923005 <dcor...@connx.comwrote:
>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.

I expect that the OP is smart enough to add additional filtering
criteria to narrow down to what he/she is specifically looking for.
>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/Researc...thods/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.
Pretty wide ranging "suggestions".

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

I think your original "try google" was more helpful ......
May 31 '07 #7

P: n/a
In article <11*********************@w5g2000hsg.googlegroups.c om>,
<dj*****@gmail.comwrote:
>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.
--
Tim Chow tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences
May 31 '07 #8

P: n/a
On May 31, 5:41 am, djhu...@gmail.com wrote:
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.
Sourceforge is usually a good pointer, but it's not so easy to answer this
particular request on there.

Indeed. Tried there also.
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/Researc...thods/MiniSat/

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.
You might try
news:comp.programming
news:sci.math.num-analysis
Perhaps this link is helpful:
http://www.lri.fr/~simon/contest/results/

May 31 '07 #9

This discussion thread is closed

Replies have been disabled for this discussion.