In an effort to learn Z3 I tried solving one of my favorite Advent of Code problems (a particularly difficult one, 2018 day 23, part 2) using the Haskell bindings sbv. Spoilers in code ahead...
module Lib
( solve
) where
import Data.SBV
puzzle :: [((SInteger, SInteger, SInteger), SInteger)]
puzzle = (\((x, y, z), r) -> ((literal x, literal y, literal z), literal r)) <$> [
((60118729,58965711,8716524), 71245377),
{- 999 more values that are large like the first one... -}
]
manhattan (a1, a2, a3) (b1, b2, b3) =
abs (a1 - b1) + abs (a2 - b2) + abs (a3 - b3)
countInRange pos =
foldr (\(nb, r) -> (+) $ oneIf (manhattan nb pos .<= r)) (0 :: SInteger) puzzle
answer = optimize Lexicographic $ do
x <- sInteger "x"
y <- sInteger "y"
z <- sInteger "z"
maximize "in-range" $ countInRange (x, y, z)
minimize "distance-from-origin" $ abs x + abs y + abs z
solve =
answer >>= print
Now, this question is not really a sbv question, nor a Haskell question and there's nothing really wrong with the above code (it solves 1000-value-puzzle lists, with huge X,Y and Z coordinates in little over a minute on my machine which is good enough for me). This question is about (0 :: SInteger) found in countInRange.
If I change (0 :: SInteger) to (0 :: SInt32) it causes the solution to take a very very long time (I kicked it off when I started typing this question and that was 16 minutes ago and counting).
So, what gives? Why is SInt32 so much slower in this case? Is it because I'm mixing domains (using SInteger elsewhere)? I would have thought that the unbounded SInteger representation would be slower than the bounded Int32.
Note that the symbolic type in question is only used for counting matching values from puzzle (thus it will always be <= 1000, i.e. the length of puzzle).
UPDATE
I killed the Int32 solution after 40 minutes of running.
When you code a problem like this in SBV, there are two places where performance can come into play:
From your description, it seems to be the latter; but you can make sure this is the case by calling optimize like this:
optimizeWith z3{verbose=True} ...
What this will do is to print the interaction SBV has with the backend solver. At some point, you'll see:
[SEND] (check-sat)
This means SBV has done its job and is now waiting for the solver to come back with an answer. Run your program again with this option turned on. If SBV is taking its time, then you'll not see the above [SEND] (check-sat) line, and that should be reported as an SBV issue here: https://github.com/LeventErkok/sbv/issues
More likely though, SBV is sending the check-sat fine, but the solver is taking much longer to respond when you use SInt32 as opposed to SInteger.
Assuming this is the case, then this is likely because your problem is much harder to solve when the underlying type is SInt32. You're doing a lot of arithmetic and asking the solver to maximize and minimize two separate goals. You can imagine that if you have unbounded Integer values, maximizing the addition of numbers might be easy to deal with: As the arguments increase so will their sum. But such is not true for SInt32: Once values start overflowing, the sum will be much lower than the arguments due to wrap-around. So, with modular arithmetic, the search space becomes much more interesting and much larger compared to the SInteger case. Bottom line is that while SInt32 has a finite representation, optimization problem over SInt32 x SInt32 x SInt32 (you have three variables), can be much more difficult due to how arithmetic works as compared to SInteger x SInteger x SInteger. In particular, the solution over SInt32 will not necessarily be the same over SInteger, again due to modular arithmetic.
Of course what happens behind the doors inside z3 is rather a black-box, and maybe they are being unreasonably slow. If you think this is the case, you might be able to report it to z3 folks as well. SBV can generate a transcript for you to send to them, when used like this:
optimizeWith z3{transcript = Just "longRun.smt2"} ...
This will create a file longRun.smt2 in SMTLib notation that can be fed to the solver outside of the Haskell ecosystem. You can file such a bug at: https://github.com/Z3Prover/z3/issues, but do keep in mind that SBV generated SMTLib files can be long and verbose: If you can reduce the problem size somehow still demonstrating the issue, that would be helpful.