Incremental STP Solving

[sreeshmaheshwar]

Does STP support incremental SMT solving techniques (e.g. reusing learned lemmas) as other solvers, like Z3 and Boolector, do? (Can't find anything in the docs about how to enable an incremental solver and haven't observed any performance differences when using push and pop in an incremental way with STP + QF_ABV + MiniSat)

If not, are there any plans for this?

[TrevorHansen]

You're right that STP doesn't keep learned clauses between invocations to the SAT solver.

It has some simple analysis, for example if a problem is unsatisfiable, and you push more frames onto it, STP knows that those problems are unsatisfiable, too.

There's lots we could do to make incremental solving faster. If you provide us with some problems that are really slow with STP ,compared to other solvers, I'll see if there's anything we can do to speed up STP's solving of them.

[sreeshmaheshwar]

Many apologies for the late reply. Thanks @TrevorHansen for your response and willingness.

Attached are some example files, using incremental querying with push/pop, for which Z3 outperforms STP, for me at least. They are KLEE generated, so sorry for the unreadability (I did try to condense them and remove redundancy but some remains) - hopefully it is not so bad that it isn't useful.

The time differences for me on my Ubuntu 20.04 machine are far more dramatic (e.g. 1.5 minutes for STP vs 1.5 seconds for Z3) though I suppose the configuration is outdated. On my Ubuntu 22.04 machine, the differences are 15.1s (STP) vs 0.7s (Z3) and 8.7s (STP) vs 0.3s (Z3). I use mainline STP throughout, with Z3 4.8.12 (22.04) and 4.8.7 (20.04).

I can produce more files that show STP being outperformed in such an incremental setting, so do let me know if that would be helpful, though my current process of printing into SMT-LIB is a bit painful. If these differences are not substantial enough and you'd like for a small number of queries that produce larger differences, I can try for that as well but I've struggled to find this so far (through KLEE).

Please let me know if there's anything else that I can help out with on this topic! I'd be very happy to see STP supporting incremental solving.

SMT-LIB2 files: dircolors.txt, b64.txt

[sreeshmaheshwar]

@TrevorHansen just wanted to friendly ping on this as I have some free time now - are these examples sufficient?

[TrevorHansen]

Thanks for the files @sreeshmaheshwar. The examples are good.

Looking at b64.txt, it's got 1000 (check-sat) calls, for me default STP takes 16 seconds, STP with simplifications disabled takes about 11 seconds, and Z3 takes about 340ms. So Z3 is about 30 times faster.

STP with simplifications disabled, is taking about 11ms per (check-sat) call, Z3 is taking about 0.34ms. These are easy problems that STP isn't optimised on. Lots of time is spent moving data to/from the SAT solver, SAT solving is about 7% of STP's total runtime.

I'm not sure what to do about this. STP doesn't do incremental solving because for hard problems it's often better to re-do the work each time - new assertions can simplify the problem, and incrementally using the SAT solver in this scenario is really hard to implement. As justification for this, STP does better head-to-head with Z3 on hard incremental problems:
https://smt-comp.github.io/2022/results/qf-bitvec-incremental

We could make an "easy" mode in STP which disables simplifications, and uses the SAT solver incrementally. Then after some timeout (e.g. 5ms) it transfers to "hard" mode which gives the current STP behaviour. But it seems easier to just wrap Z3 and STP in a script that does the same thing (i.e. use Z3 as the easy-mode).

It makes me wonder if you occasionally get problems that are hard for Z3 to solve?

[sreeshmaheshwar]

Thanks for the response @TrevorHansen.

Indeed, Z3's incremental solver that is used for these benchmarks performs worse on harder problems due to lack of pre-processing. See the examples linked in the relevant discussion Z3Prover/z3#7203 where, as a result, I was confused by the outperformance of Z3's incremental solver when used non-incrementally in mainline KLEE. It also suggests that such hard problems are rarer in KLEE - though I will keep an eye out for slower queries during longer runs.

The two benchmarks I provided in our current discussion are from my experimental fork of KLEE. This incremental work is experimental and concludes shortly, so I should clarify that there is no concrete need for STP incrementality yet (from KLEE), in the case that it is difficult to implement or not worth it in your opinion. As an aside, you mention an incremental solver that switches to a non-incremental one after a timeout - this is supported by Z3.

Speaking of mainline KLEE, your suggestion of timeout-based portfolio solving using Z3's incremental (but used non-incrementally) solver and STP's (normal) solver generalised seemed to me to be a near-optimal KLEE configuration. But I'll try to run some more experiments to confirm this. Thanks for the suggestion.