Why is Int32 sort much slower than Integer sort in this SBV/Z3 code?

Question

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.

Kreis

I don't have much of a clue about this, but anyway I wonder what happens if you change everything to SInt32. – Compliance

Good question @duplode, I can try that after it finishes (if it finishes). I'm afraid that manhattan may overflow with SInt32 but I haven't done the analysis to prove that. – Kreis

@Compliance All SInt32 seems slower as well. It's been running for 3 minutes as of this comment. – Kreis

Try it like this: optimizeWith z3{verbose=True}. This'll show you when SBV sends the query to z3 and waits for the answer. (You'll see a line [SEND] (check-sat) and SBV waiting for an answer from z3.) Where is the slow down? Is it that SBV doesn't send the (check-sat) request as quickly, or is it the solver that's taking much longer to respond to check-sat? – Matte

Can you use the API of Z3 to generate the SMT-LIB version of both encodings? I am curious to try it out with other solvers. – Legg

I have no real idea, but here's a guess: maybe with SInt32 the solver has to cope with overflow, which makes the constraints harder to solve, due to the more complex underlying math. – Afar

Answer 1

When you code a problem like this in SBV, there are two places where performance can come into play:

• SBV might be taking a long time to produce the query itself
• SBV sends the query to the solver fine, but the solver is taking a long time to respond

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.

Matte

Thanks alias, great answer! [SEND] (check-sat) is sent fairly quickly (though seemingly more quickly with SIntegers). I think you're probably right about the Int32 expense. The verbose outputs are super useful tricks, thanks so much! – Kreis