5

For a project I'm starting I will need to use a SAT solver. I've used some of them before but mainly for experimenting, while here the main constraint for the project is good performance. I'm trying to look for alternatives, and trying to understand how each alternative is positioned regarding my specific requirements. In particular:

  1. I'll need to extract the satisfying assignments, not only checking for satisfiability, and the solver should allow me to repeatedly solve the same formula looking for different possible satisfying assignments, eventually iterating over all of them, in an efficient way (e.g. without me having to add a clause and start all over again).

  2. The project should be still actively maintained and fairly production-quality, not some competition-winning research project abandoned since the publication (see picosat).

  3. Moreover, since I'm using C++, the solver should provide an efficient and (possibly) good written C++ interface.

The first candidate I considered was Z3, but I'm confused by the docs and cannot understand if point 1. above is supported, and if it might be overkill given that I only need SAT and not SMT. The C++ interface also seems very easy to use but I can't stand the fact that I have to name the variables with plain strings (this pairs very badly with my surrounding algorithm. Isn't it avoidable?).

So can you give me some suggestion on which SAT solver to use, or shed some light on by doubts regarding Z3?

gigabytes
  • 3,104
  • 19
  • 35
  • Never used it but I ever heard about it : http://minisat.se/ – Fefux Dec 09 '16 at 09:54
  • (1a) You can extract models from Z3: cf. http://rise4fun.com/Z3/tutorial/guide and search for `get-model` (1b) Extracting different models is possible but requires a manually-written solving loop, cf. http://stackoverflow.com/questions/13395391 – Malte Schwerhoff Dec 09 '16 at 10:03
  • @Fefux thanks. While `minisat` is good for experimenting, it is the kind of unmaintained research project I was talking about. It is also quite old. – gigabytes Dec 09 '16 at 10:23
  • @MalteSchwerhoff thanks. Do you know if it is possible to avoid using strings to name the variables? I'd rather prefer integer IDs. – gigabytes Dec 09 '16 at 10:25
  • 1
    [**z3**](https://github.com/Z3Prover/z3) is more than a *SAT* solver, it's a *SMT* solver like, e.g., [Yices](http://yices.csl.sri.com/), [cvc4](http://cvc4.cs.nyu.edu/web/) and [mathsat5](http://mathsat.fbk.eu/). See [sat competition](http://www.satcompetition.org/) and [smt competition](http://smtcomp.sourceforge.net/2016/) for more solvers. Some solvers provide an *all-sat* interface, returning all possible solutions. However, you can do this with any solver by simply incrementally call *solve()* after adding to the formula the negation of the previous model. – Patrick Trentin Dec 09 '16 at 11:47
  • @PatrickTrentin yes, but the solver needs to be stateful, such that the second call don't start repeating all the work but can incrementally proceed the search. Anyway, I'll look a the sat competition, but I was looking for some advice because the list is rather long, and there's no indication of whether the solver is just a research prototype or a production-quality product. – gigabytes Dec 09 '16 at 12:11
  • 1
    There's plenty of incremental *SAT* and *SMT* solvers out there, I think all of those I named are, which means they keep learned clauses around across subsequent searches. After learning the *negation* of the previous model you cause a search restart from *level 0* anyway, so *AFAIK* it makes *little* difference whether you implement this scheme externally or use one which has direct support for that. Since I have a conflict of interests, I must refrain from making suggestions for a specific tool. You can consider **z3** *production-quality* level, just like many others. – Patrick Trentin Dec 09 '16 at 12:16
  • 1
    As you say, Z3 may be overkill. However, it does support integer-numbered variables; Z3_mk_const takes a symbol (not a string) and you can create integer-numbered symbols via Z3_mk_int_symbol. – Christoph Wintersteiger Dec 09 '16 at 15:33
  • @ChristophWintersteiger oh I see... So is the C++ API simply lacking support for this feature? – gigabytes Dec 09 '16 at 17:42
  • The C++ API only provides some convenient features like expr classes to take care of the reference counting. It's intended to be used in combination with the C API. However, for this particular case, it does provide context::int_symbol(int n). – Christoph Wintersteiger Dec 10 '16 at 13:00
  • Ah I see. Thank you. Talking about Z3 being "overkill": that's the topic of the question. Any hint for a fast production-quality SAT solver? – gigabytes Dec 10 '16 at 13:02
  • 1
    @gigabytes It would be great if you could report back on your findings, e.g. if you got around to compare the solvers that participated in SAT and SMT competition (as suggested by Patrick) – Malte Schwerhoff Dec 13 '16 at 10:17
  • Yes, I'll write an answer when I'll manage to do the comparison :) – gigabytes Dec 13 '16 at 11:40
  • @gigabytes Did you try to look at Answer Set Programming and #SAT solvers? They enumerate all possible solutions for a given formula. I would recommend [Potassco](https://potassco.org) solver as a starting point, however, I'm not sure how good is it's API. I used [sharpCDCL](http://tools.computational-logic.org/content/sharpCDCL.php) to solve some real-world problems. It was perfect match to my demands, but in terms of API it's basically minisat. – CaptainTrunky Mar 08 '17 at 06:10
  • @gigabytes And, by the way, try to look at [Glucose](http://www.labri.fr/perso/lsimon/glucose/) solver. It's based on MiniSat and well maintained. It have shown the best performance in my own projects (except for in-house commercial solver). – CaptainTrunky Mar 09 '17 at 02:48
  • @CaptainTrunky that looks interesting, thanks! – gigabytes Mar 09 '17 at 07:35

1 Answers1

1

If you are willing to put some work into fixing build for different platforms (or don't need them at all), MiniSat's interface is rather nice. Do note that it is not really maintained anymore though.

There is also Glucose, which shares MiniSat's interface and is relatively actively maintained. It also performs quite a lot better in SAT competitions than MiniSat does.

Before choosing one or the other, you need to understand is that while Glucose generally wins over MiniSat in SAT competitions, your use case might not be solving SAT competitions. As an example, our project generally generates satisfiable formulas, where the task is to find one of (usually) many SAT assignments and MiniSat usually outperforms Glucose there. OTOH if your project mostly generates unsatisfiable formulas or formulas with a single solution to be found, Glucose will likely do better, as it is optimized for quickly finding UNSAT proofs, rather than finding SAT assignments.

One more solver that I've had experience with embedding is CryptoMiniSat. It has a reasonable C++ interface and is very actively maintained. When I had an issue or bug, it usually was fixed inside a week. However it provides stable releases rarely, so if you are using it you will likely end up living off a specific hash rather than a proper release.

One more thing to note: Glucose provides a parallel solver but with a rather interesting licence. CMSat provides parallel solver under MIT licence. MiniSat has a very liberal licence, but no parallel option at all.

Xarn
  • 3,460
  • 1
  • 21
  • 43