12
$\begingroup$

I am trying to solve a 25k clauses 5k variables SAT problem. As it has been running for an hour (precosat) and I'd like to solve bigger ones afterwards, I'm looking for a multi-core SAT-Solver.

As there seem to be many SAT-Solvers, I'm quite lost.

Could anyone point me out the best one for my case?

I'd also be happy if someone could give me the approximate time (if possible).

$\endgroup$
  • 1
    $\begingroup$ You are looking for ready-made programs? Then this is not the best site to ask. You want to learn about SAT-solving? Welcome! You say you have searched; what did you find? What confuses you? $\endgroup$ – Raphael Nov 15 '13 at 14:52
  • $\begingroup$ Well, I looked at the number of SAT-related threads on several StackExchange forums. I ended up having too choose between theoretical CS and CS (and choose the later). Where should have I asked for a ready-name program? Thanks. $\endgroup$ – multsatsolv Nov 16 '13 at 13:04
8
$\begingroup$

Have a look at the results from this years SAT 2013 competition. Based on these results, definitely give Lingeling a try. Plingeling is the parallel variant of it.

If you don't need to prove unsatisfiability (perhaps you know the instance is satisfiable, and you just need to know an assignment making it SAT), you could try local search methods, too.

$\endgroup$
  • $\begingroup$ Thanks. I'll have a look at (P)Lingeling. Also, I have no idea if it is satisfiable (although it better be, otherwise I'm stuck). $\endgroup$ – multsatsolv Nov 14 '13 at 17:18
  • $\begingroup$ +1. Based on our experience, plingeling is certainly what you should try first (at least if you have a single computer with multiple cores and plenty of memory). For even more performance, try to find a computing cluster with as many nodes as possible and run multiple instances of lingeling (or plingeling) with different random seeds. $\endgroup$ – Jukka Suomela Nov 15 '13 at 20:52
4
$\begingroup$

I'm not sure about the existence of practical multicore sat-solvers, but there are a few projects and papers:

I also found this interesting point: you can run a regular sat-solver multiple times with different seeds on the same problem in parallel, to get a multi-core effect.

Edit: Incorporating my comments on vzn's idea here:

A similar alternate method is to simply choose a single variable, set its value to true, send that to one solver instance. Set its value to false, and send that to another solver instance. You can do this for $k$ variables, and run $2^k$ processes simultaniously. Choosing the variables to set could be a little tricky, ie. if they are directly dependent on each-other, then it is pointless to choose one and then another. A simplification step might be necessary to do successive/recursive choices.


(I'd also be happy if someone could give me the approximate time (if possible) to solve an X clauses Y variables SAT problem.)

No one can give you an approximate time based on $m$ variables, $n$ clauses, because some SAT problems are extremely difficult (read: not gonna happen) to solve, even with a relatively small $m,n$; while other huge instances can be solved relatively quickly (and it is for these instances that sat solvers are useful).

$\endgroup$
  • $\begingroup$ Thanks for the links. I'll read some of them. I hope my problem is not too hard to solve though. $\endgroup$ – multsatsolv Nov 14 '13 at 17:22
  • $\begingroup$ @multsatsolv it depends on the problem. It also depends on the encoding. SAT solvers can handle different encodings of the same problem differently. And different SAT solvers might be better at one encoding than another; there is no science to this (well there is, but it is beyond worth trying to understand, in the fast-paced evolution of SAT solvers): the only thing to do is try different combinations of encodings and solvers. $\endgroup$ – Realz Slaw Nov 14 '13 at 19:28
3
$\begingroup$

There is actually a very simple way to turn any SAT solver into a parallel version because SAT is embarrassingly parallel in the following sense.

Choose some power of two to partition it by, $2^n$. Then choose $n$ variables and assign all possible boolean values. There will be $2^n$ resulting SAT formulas after the assignments. Solve each one separately (in parallel). There is an overall solution iff one of the separate solutions exists and the full solution is exactly the union of all the separate solutions.

$\endgroup$
  • $\begingroup$ $n$ is usually pretty large (it is a min-cut on the clause-variable graph, and it is probably always larger than the backdoor). A similar alternate method is to simply choose a single variable, set its value to true, send that to one solver instance. Set its value to false, and send that to another solver instance. You can do this for $k$ variables. Choosing the variables to set could be a little tricky, ie. if they are directly dependent on each-other, then it is pointless to choose one and then another. A simplification step might be necessary to do successive/recursive choices. $\endgroup$ – Realz Slaw Nov 15 '13 at 18:51
  • 3
    $\begingroup$ This approach does not seem to work too well in practice. For positive instances the following approach is typically much better if you have lots of computers: simply run e.g. lingeling with the same instance but different random seeds and wait until one of the solvers finds a solution. $\endgroup$ – Jukka Suomela Nov 15 '13 at 20:45
  • $\begingroup$ @jukka which approach & why doesnt it work too well? is it due to imbalance in workload? rs has a good point about the partition not nec splitting up the workload very equally but that will tend to depend on (symmetry in) instance structure, and he he points out its easy to initially choose variables that seem to partition it more equally as far as evening out resulting # of clauses. realz, didnt understand the point about $n$ vs the backdoor... think backdoors are prob rare in truly hard instances... $\endgroup$ – vzn Nov 15 '13 at 21:26
  • 1
    $\begingroup$ @vzn: The approach that you suggested. To see why it doesn't work too well, try it out with real-world instances and compare it with what I suggested. :) Your approach would make a lot of sense if you were dealing with a naive backtracking search algorithm, but modern SAT solvers are much more than naive backtracking search. $\endgroup$ – Jukka Suomela Nov 16 '13 at 0:32
  • $\begingroup$ fine but can you explain in words what the issue is? your approach may work for satisfiable instances ok but wouldnt it take exactly the same time in parallel to discover an unsatisfiable instance no matter how many separate instances are run? if not, maybe there is a ref to cite on the subj... $\endgroup$ – vzn Nov 16 '13 at 1:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.