No output from Z3/SMT solver for weight balancing problem with nested quantifiers

Question

Let Z3 solve the following puzzle: You have a balance scale with four weights. With these four weights you must balance any whole number load from 1kg all the way up to 40kg. How much should each of the four weights weigh? (You may place weights on both sides of the scale.) (source: https://www.mathsisfun.com/puzzles/only-4-weights.html)

I was wondering why this code in z3 is not giving any ouput, after a certain time I get unkown as output. There is probably a better solution for this assignment, but am I doing something wrong or is it to difficult for z3 to solve this with my constraints?

; the four weights
(declare-const w1 Int)
(declare-const w2 Int)
(declare-const w3 Int)
(declare-const w4 Int)

(assert (and

    (<= 1 w1 40)
    (<= 1 w2 40)
    (<= 1 w3 40)
    (<= 1 w4 40)

    ; for every kilo from 1 to 40 it has to balance with the 4 weights
    ; weight can be multiplied with 1, this means it is on the opposit side of i
    ; weight can be multiplied with -1, this means is on the same side of i
    ; weight can be multiplied with 0, this means the weight won't be used
    (forall ((i Int))
        (implies
            (<= 1 i 40)
            (exists ((j Int) (k Int) (l Int) (m Int))
                (and
                    (<= -1 j 1)
                    (<= -1 k 1)
                    (<= -1 l 1)
                    (<= -1 m 1)
                    (= i (+ (* w1 j) (* w2 k) (* w3 l) (* w4 m)))
                )
            )
        )
    )
))

(check-sat)
(get-model)

Answer 1

You've a few discrepancies between what you described and what you coded. For instance, you only allow i to range between 1 and 10; though I think you meant 1 and 40. Similarly, you allow j, k, l, and m to be just 0 or 1, though you probably meant them to range over -1, 0, and 1.

All of that, however, is tangential. Even when you fix those issues, you will still have the complexity problem: SMT solvers aren't good at reasoning with quantifiers. Even though the search space isn't very big for this particular problem, the internal heuristics fail to recognize that; causing it to take too long, or loop forever. Instead, you should "expand" all the possibilities yourself and present a quantifier-free version of your problem.

Unfortunately, programming these sorts of constraints is hard to do with SMTLib, because it's really not meant for this kind of programming. Instead, I'd recommend using a higher-level API for z3 to address the problem instead. That is, use one of the z3 bindings from Python, Haskell, C, C++, Java, etc.; whichever you're more comfortable with, instead of coding this directly in SMTLib.

Below, I'll code it using SBV (the Haskell interface for z3), and also using the Python interface for z3; as those are the APIs I'm most familiar with.

Haskell

Using SBV (See http://leventerkok.github.io/sbv/ and https://hackage.haskell.org/package/sbv) and a bit of Haskell magic, you can code your problem as:

import Data.SBV

allCombs :: [a] -> [([a], [a], [a])]
allCombs []     = [([], [], [])]
allCombs (x:xs) = concat [[(x:l, m, r), (l, x:m, r), (l, m, x:r)] | (l, m, r) <- allCombs xs]

weigh :: ([SInteger], [SInteger], [SInteger]) -> SInteger
weigh (left, _, right) = sum left - sum right

pick :: IO SatResult
pick = sat $ do
        w1 <- sInteger "w1"
        w2 <- sInteger "w2"
        w3 <- sInteger "w3"
        w4 <- sInteger "w4"

        -- All weights must be positive
        constrain $ w1 .> 0
        constrain $ w2 .> 0
        constrain $ w3 .> 0
        constrain $ w4 .> 0

        -- Symmetry breaking: Order the weights. Strictly speaking this isn't
        -- necessary, but helps with presentation
        constrain $ w1 .<= w2
        constrain $ w2 .<= w3
        constrain $ w3 .<= w4

        let combs  = map weigh (allCombs [w1, w2, w3, w4])
            find g = sAny (.== literal g) combs

        constrain $ sAnd $ map find [1..40]

This essentially takes all possible orderings of the four weights into three groups: Those that are added, those that are ignored, and those that are subtracted. Then it asks the solver to find a combination that can achieve the summation for any value between 1 and 40. When I run this, I get the following answer fairly quickly:

*Main> pick
Satisfiable. Model:
  w1 =  1 :: Integer
  w2 =  3 :: Integer
  w3 =  9 :: Integer
  w4 = 27 :: Integer

And you can convince yourself that this is a good setting for the weights. (In fact, you can show that this is the only solution, by changing the call sat to allSat, and you'll see that SBV confirms this is the only solution.)

Python

The idea is similar, though Python code looks uglier (of course, this is a subjective claim!):

from z3 import *

def allCombs(lst):
    if not lst:
        yield ([], [], [])
    else:
        cur = [lst[0]]
        for (add, ign, sub) in allCombs (lst[1:]):
          yield (cur + add, ign, sub)
          yield (add, cur + ign, sub)
          yield (add, ign, cur + sub)

def weigh(comb):
    return sum(comb[0]) - sum(comb[2])

s = Solver()
w1, w2, w3, w4 = Ints('w1 w2 w3 w4')
s.add(w1 > 0)
s.add(w2 > 0)
s.add(w3 > 0)
s.add(w4 > 0)
s.add(w1 <= w2)
s.add(w2 <= w3)
s.add(w3 <= w4)

allSums = [weigh(comb) for comb in list(allCombs([w1, w2, w3, w4]))]

def constrain(goal):
    s.add(Or([goal == s for s in allSums]))

for i in range(40):
    constrain(i+1)

print(s.check())
print(s.model())

And this prints:

sat
[w1 = 1, w2 = 3, w3 = 9, w4 = 27]

This is the same solution z3 found via the SBV API.