Offering an effective SAT solution with a good C ++ interface (or: Z3 is right for me)?

Question

For the project that I am launching, I will need to use the SAT solver. I used some of them before, but mainly for experimentation, while the main obstacle for the project here is good performance. I try to find alternatives and try to understand how each alternative is positioned in relation to my specific requirements. In particular:

• I will need to extract satisfactory tasks, and not just check for feasibility, and the solver should allow me to repeatedly solve the same formula that searches for various possible satisfying tasks, ultimately iterating over all of them, in (for example, without having to add a sentence and start all over again).

• The project should continue to be actively supported, and the quality of production, and not some victorious research project left after publication (see picosat ).

• In addition, since I use C ++, the solver should provide an efficient and (possibly) good written C ++ interface.

The first candidate I considered was Z3, but I am confused by the docs and can't figure out if clause 1. is supported above, and if that might be redundant, given that I only need SAT, not SMT. The C ++ interface also seems very easy to use, but I can’t hold back the fact that I have to name the variables using simple strings (this is very bad with my surrounding algorithm. Can it be avoided?).

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

Answer 1

If you want to make some corrections to the assembly for different platforms (or are not needed at all), the MiniSat interface is pretty nice. Keep in mind that it really is not supported anymore.

There is also Glucose , which shares the MiniSat interface and is relatively actively supported. He also performs much better in SAT competitions than MiniSat.

Before choosing one or the other, you need to understand that although Glucose usually wins MiniSat in SAT competitions, your use case may not solve SAT competitions. As an example, our project usually generates executable formulas, where the task is to find one of the (usually) many SAT prescriptions, and MiniSat usually outperforms Glucose. OTOH, if your project basically generates unsatisfactory formulas or formulas with one solution found, glucose is likely to be better because it is optimized to quickly search for UNSAT evidence rather than determining SAT prescriptions.

Another solver I encountered with the implementation is CryptoMiniSat . It has a reasonable C ++ interface and is very actively supported. When I had a problem or error, it usually was fixed after a week. However, it rarely provides stable releases, so if you use it, you will most likely end up with your own hash rather than the correct release.

One more note: Glucose offers a parallel solver, but with a rather interesting license. CMSat provides a parallel solver under the MIT license. MiniSat has a very liberal license, but does not have a parallel version.