all-sat performance

[LeventErkok]

For this program:

f : (Integer, Integer, Integer) -> Bit
f (x, y, z) =  inRange x && inRange y && inRange z
  where inRange v = (1 <= v) && (v <= 15)

The current SBV backend finds all solutions in about 20 seconds:

Main> :set satNum=all
Main> :sat f
.....
(Total Elapsed Time: 20.854s, using "Z3")

The w4 backend seems to be about 15 times slower:

Main> :set satNum=all
Main> :set prover=w4-z3
Main> :sat f
.....
(Total Elapsed Time: 5m:23.774s, using "z3")

I'm not sure why there's such a big discrepancy; perhaps something to look at.

Furthermore, the new SBV release (v8.13) (https://hackage.haskell.org/package/sbv-8.13) has an improved allSat algorithm. To wit:

Prelude Data.SBV> :set +s
Prelude Data.SBV> allSat $ \x y z -> sAnd [1 .<= i .&& i .<= 15 | i <- [x, y, z::SInteger]]
....
Found 3375 different solutions.
(2.49 secs, 614,674,952 bytes)

Which is about 8 times faster than the previous SBV algorithm, and about 130 times faster than the w4-z3 backend as it stands.

You can get a performance boost simply by upgrading to SBV8.13 of course; but for w4 maybe you also want to implement the faster algorithm, which is described at: http://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations

[robdockins]

Thanks for the link, I'll definitely be interested in learning about it. As to the performance difference, that's absolutely something I'm interested in tracking down.

[robdockins]

Speculative hypothesis: the What4 backend is currently slow for all-sat because it spawns a separate solver process for each subsequent query instead of doing incremental solving, whereas I think SBV is doing incremental solving in these cases. We know from experience that the process creation overhead alone can be quite significant in cases like this. We should probably switch over to using incremental solving modes for the solvers that support them.

[LeventErkok]

That's correct. SBV uses incremental mode for allSat. In fact, the newer algorithm in v8.13 crucially depends on this, since it also uses push and pop to judiciously to dissect the search space into disjoint subsets, which gives the an-order-of-magnitude speed boost.