Home     |     .Net Programming    |     cSharp Home    |     Sql Server Home    |     Javascript / Client Side Development     |     Ajax Programming

Ruby on Rails Development     |     Perl Programming     |     C Programming Language     |     C++ Programming     |     IT Jobs

Python Programming Language     |     Laptop Suggestions?    |     TCL Scripting     |     Fortran Programming     |     Scheme Programming Language


 
 
Cervo Technologies
The Right Source to Outsource

MS Dynamics CRM 3.0

C Programming Language

2SAT in C


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

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.

In article <1180553658.423749.84@p47g2000hsd.googlegroups.com>,

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

On 30 May 2007 22:18:14 GMT, in comp.lang.c , t@lsa.umich.edu
wrote:

>In article <1180553658.423749.84@p47g2000hsd.googlegroups.com>,
>user923005  <dcor@connx.com> wrote:
>>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

On May 30, 3:18 pm, t@lsa.umich.edu wrote:

> In article <1180553658.423749.84@p47g2000hsd.googlegroups.com>,

> user923005  <dcor@connx.com> wrote:
> >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/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.

> 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/Research/FormalMethods/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

Pretty wide ranging "suggestions".

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

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

In article <1180615285.000960.83@w5g2000hsg.googlegroups.com>,

 <djhu@gmail.com> wrote:
>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

On May 31, 5:41 am, djhu@gmail.com wrote:

You might try
news:comp.programming
news:sci.math.num-analysis
Perhaps this link is helpful:
http://www.lri.fr/~simon/contest/results/
Add to del.icio.us | Digg this | Stumble it | Powered by Megasolutions Inc