Suggestion of an efficient SAT solver with good C++ interface (or: is Z3 good for me)?

Question

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?

Answer 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.