Make Minisat optional?

[TrevorHansen]

Is there any reason to keep STP using Minisat or Simplifying Minisat?

Personally, I never use STP with Minisat. There are such better solvers, like CryptoMinisat, that I'd rather people used.

Minisat is also annoying because it keeps causing build problems.

What do people think about removing Minisat support from STP?

[aytey]

At the very least (and I'm not saying that this is a reason not to remove Minisat, but just a data-point), but it seems that KLEE's documentation only talks about building STP with Minisat:

• https://klee.github.io/build-stp/
• https://github.com/klee/klee/blob/64dfbcd7073e0286e8c0145e1750f9fe3abc7565/Dockerfile#L30

and, worse, KLEE's build scripts explicitly disable CMS:

• https://github.com/klee/klee/blob/64dfbcd7073e0286e8c0145e1750f9fe3abc7565/scripts/build/p-stp.inc#L66

We could ask the STP team how they feel about this? Maybe they have a reason they use Minisat vs. CMS.

[251]

From the KLEE side: CryptoMinisat in the past has been really slow in comparison to MiniSat for my benchmarks and I refrained from using it. However, I did a quick benchmark run recently and it doesn't seem to be the case anymore (klee/klee#1480 (comment)). If it's not too much a maintenance burden I'd vote for keeping MiniSat - makes it easier to reproduce results from other papers but we are also able to update the docs and build scripts. ;)

[TrevorHansen]

Thanks @251.

How does this sound to people?

• STP can be used with Minisat.
• STP can be built without Minisat, but it can't be built without a modern solver (e.g. Cryptominisat).
• STP's default will be to use the modern solver, unless Minisat (or simplifying minisat) is chosen at run-time.

[aytey]

Currently we require MiniSat and CMS is optional -- are we considering swapping this? Basically, are we going to default to MiniSat being off? I'd vote for this option, because MiniSat seems to cause the most number of GitHub issues (due to clashes between our MiniSat and a system-installed one).

I wonder if we should have a build-time configuration to set the default solver? This would mean that downstream tools (e.g., KLEE) could build STP with something like -DUSE_MINISAT:BOOL=ON -DDEFAULT_SAT_SOLVER:STRING=MINISAT, which would them give them a build that functions the same as we currently have (with the exception that we do now always link against CMS).

[aytey]

can't be built without a modern solver (e.g. Cryptominisat).

Do you mean "e.g." there or "i.e."? Basically, if you mean "e.g.", then are you suggesting STP could be built with only Riss?

[TrevorHansen]

Thanks @aytey.

Do you mean "e.g." there or "i.e."? Basically, if you mean "e.g.", then are you suggesting STP could be built with only Riss?

Nicely spotted. For modern solvers, I was thinking CMS, Riss or Cadical (there's a branch supporting Cadical).

Basically, are we going to default to MiniSat being off?

Yeah, that was what I'm thinking. I'd like to de-emphasise Minisat. Like you say it causes build problems and in my experience has been eclipsed by modern SAT solvers. I wouldn't want someone building STP with minisat and expecting it to solve hard problems.

I wonder if we should have a build-time configuration to set the default solver?

This isn't something I'd personally use, but if your or someone else wants to do it, I can imagine it being helpful.

Thinking more about it. How does this sound?

• STP can be built without Minisat.
• STP can be used with Minisat still.
• STP requires 1 or more modern SAT solver to link to (i.e. CMS, Cadical or Riss).
• STP's default will be to use the modern solver, unless Minisat (or simplifying minisat) is chosen at run-time. (Unless someone else makes it selectable at build time like @aytey suggests).
• Our documentation will be updated to remove reference to building STP with minisat, and instead suggest using CMS.

[251]

STP requires 1 or more modern SAT solver to link to (i.e. CMS, Cadical or Riss).

Why would you make it a requirement and not just a warning (during build and in the docs)?

there's a branch supporting Cadical

Nice, are you going to merge it?

[aytey]

This isn't something I'd personally use, but if your or someone else wants to do it, I can imagine it being helpful.

I also wouldn’t use this, but it was trying to make life easy on downstream tools that expect, by default, to have MiniSat — making that a build-time change means that no “application code” needs to change to get the same behaviour from STP.

STP requires 1 or more modern SAT solver to link to (i.e. CMS, Cadical or Riss).

Does this restriction matter? I mean, why couldn’t MiniSat be in this list?

What I’m trying to say is that if someone really wants a build of STP with only MiniSat, then let’s not block them from having it.

How does this sound?

I think the crux of what we want to do should be:

• make MiniSat be optional

• require at least one SAT solver (obviously 🤣)

• make it clear in our documentation that we recommend CMS/Riss/CaDiCaL, but MiniSat is an option

This is close to your list, but doesn’t force someone to have a “modern” SAT solver.

[aytey]

I should add: it might seem I’m really keen to keep MiniSat — I’m totally down to remove it totally, but I also understand that some of our users (e.g., KLEE, as per this issue and the linked KLEE issue) really still consider MiniSat to be the best choice for them.

[rgov]

There's always the option for those who wish to continue using Minisat to build against an older release of STP that still supports it. This might be fine for "reproduc[ing] results from other papers"? If we decide to keep it around now, are we going to be revisiting the same question 3 or 5 years from now?

[aytey]

@rgov what do you think about not allowing people to use MiniSat as the "only" option though?

I still don't know why we'd make MiniSat be the only solver we support that requires "another" solver (e.g., I'm presuming we will allow STP to built with only CMS, but I think that @TrevorHansen's suggestion is that if you wanted MiniSat, then you have to have another solver too).

Apologies to @TrevorHansen if I've misrepresented his idea ...

[rgov]

It sounds more complicated—and increases the complexity of our build scripts etc.—than just eliminating MiniSat and saying, "Use version x.yy if you absolutely need MiniSat. This version is deprecated, and support requests may be unanswered." We already provide a Dockerfile that builds it in a reproducible way so this shouldn't be too much of a burden.

[aytey]

Okay, so if we're totally killing MiniSat, then let's do it -- but I think a half-way house where MiniSat is a weird "half supported" solver makes things more complicated than needs be.

[251]

"Use version x.yy if you absolutely need MiniSat. This version is deprecated, and support requests may be unanswered."

This is bad from a user's perspective. STP is packaged typically with minisat and cryptominisat (sometimes even just with minisat as in Thumbleweed) and that means on all these systems the behaviour changes without a fall-back option. Just announce minisat is deprecated everywhere, let users fix/test the new back-end and revisit the decision in 3 years as proposed above.

[rgov]

This is bad from a user's perspective.

Ok, we could continue giving support (insofar as we are volunteers who do our best to help people when they get stuck, and maybe backport fixes to egregious issues), but I don't see a problem with killing support in future releases while past releases (e.g., 2.3.4) continue to work as they ever did—that is the fallback option. Users who don't want surprise behavior changes shouldn't be installing new versions, especially with version number jumps that warn of breaking changes (e.g., 2.4).

[aytey]

Could we make it optional and deprecated (while still not requiring another solver)? If anyone asks for support on GitHub for MiniSat-related issues we say "sorry, MiniSat is unsupported, use CMS/CaDiCaL/Riss"?

If Ryan/Trev care strongly about this (and I don't), then I'm fine to kill it off.

[TrevorHansen]

Thanks for everyone's input.

I came into the conversation believing that it is better to use a modern solver vs Minisat with STP on any problem type. This is driven largely by my experience solving hard problems. For instance, I read this graph to say a modern solver is about 30 times faster than Minisat:

I understand now that people use STP to solve lots of easy problems. I hadn't considered this, and even though I haven't seen any examples yet where CMS is slower than Minisat, it's now plausible to me that it happens.

Given how slow Minisat is compared to modern solvers, I don't want users inadvertently using it. Requiring users to have a modern SAT solver, which is the default, built with STP seems to me the best way to do that. This also has the advantage that it makes it easy for users to compare Minisat's performance to a modern solver - because it's already built with STP, and then hopefully report slowdowns to us so that we can fix them.

I've learned a lot during the discussion, and hope people feel OK with making a modern SAT solver mandatory. Given, of course, that we're open source, so users can edit our build scripts to run whatever SAT solver they want.

[aytey]

Sounds good to me, @TrevorHansen!

[2994186010]

@TrevorHansen ，Where is a STP branch supporting Cadical?

Nicely spotted. For modern solvers, I was thinking CMS, Riss or Cadical (there's a branch supporting Cadical).

[aytey]

@2994186010: the branch is here -- https://github.com/stp/stp/tree/cadical