►CMSC 433:   Programming Language Technologies and Paradigms
▼Notes
►12 Solving SAT and SMT Problems Using Z3
On this page:
12.1 Review of Logical Operators
12.2 SAT & SMT
12.3 Solving Puzzles with SMT
12.4 Rabbits and Chickens
12.5 Cats and Dogs
12.6 Sudoku
12.7 Sum of Two Real Numers
12.8 Coin Sum
12.9 8 Queens Puzzle
12.10 Circle, Square, and Triangle
12.11 De Morgan’s laws
12.12 Integer Overflow
12.13 Wedding Seating
8.17
    contents    up   

12 Solving SAT and SMT Problems Using Z3🔗

    12.1 Review of Logical Operators

    12.2 SAT & SMT

    12.3 Solving Puzzles with SMT

    12.4 Rabbits and Chickens

    12.5 Cats and Dogs

    12.6 Sudoku

    12.7 Sum of Two Real Numers

    12.8 Coin Sum

    12.9 8 Queens Puzzle

    12.10 Circle, Square, and Triangle

    12.11 De Morgan’s laws

    12.12 Integer Overflow

    12.13 Wedding Seating

Before you start this section, make sure have a Python 3 installation available. You can check if this is the case by running python3, which should open a Python session.

You will also need to install the Z3 SMT solver and its Python bindings. Please follow the instruction at Insatll Z3 to install Z3 solver.

Now to check that everything was correctly installed, start a Python session and run: 

from z3 import *

12.1 Review of Logical Operators🔗

First, we’ll do a quick review of some useful logical operators.

  • And(x, y) is true iff x and y are true.

  • Or(x, y) is true iff x or y are true.

  • Not(x) is true iff x is false.

  • Implies(x, y) (x ==> y) is true iff x is true implies that y is true.

It is common to write truth tables to describe the behavior of these operators.

We show the tables for And, Or, and Implies below.

And

Or

Implies

a

 

b

 

a && b

true

 

true

 

true

true

 

false

 

false

false

 

true

 

false

false

 

false

 

false

a

b

a || b

true

true

true

true

false

true

false

true

true

false

false

false

a

b

a ==> b

true

true

true

true

false

false

false

true

true

false

false

true

12.2 SAT & SMT🔗

Suppose we want to find a satisfying assignment for the expression (a || !b) && (!a || c). That means we’re looking for values of a, b, and c that make the entire expression evaluate to true.

One way to approach this is by checking all possible combinations of truth values for a, b, and c. Since each variable can be either true or false, there are 2^3=8 possible combinations.

Can you list all 8 combinations of a, b, and c?

In general, for n variables, there will be 2^n possible assignments, so the approach of "trying everything" is not efficient for large n. In fact, this is the SAT ("satisfiability") problem, which is NP-complete, meaning that it is "one of the hardest problems to which solutions can be verified quickly. But this difficult problem is exactly what tools like the Z3 SMT solver! Here’s how we can solve the problem using the Z3:


from z3 import *
a = Bool('a')
b = Bool('b')
c = Bool('c')

s = Solver()
s.add(Or(a, Not(b))) # a || !b
s.add(Or(Not(a), c)) # !a || c
s.check() # do these equations have a solution?
s.model() # get the solution

# Output: [b = False, a = False, c = False]

The output says that the formula (a || !b) && (!a || c) will be true when a, b, and c are all false.

But what if we want a different solution?

In this case, we can add an additional constraint that says that we don’t want the solution where a, b, and c are all false.


s.add(Not(And(Not(a), Not(b), Not(c))))
s.check()
s.model()

# Output: [b = False, c = True]

This output says that the formula (a || !b) && (!a || c) will be true when b is false and c is true (it doesn’t matter what a is).

Let’s try adding one more constraint: 


s.add(And(Not(a), b))
s.check()

# Output: unsat

The output unsat means unsatisfiable. The solver is telling us that there is no possible choice of a, b, c that makes the current constraints true.

Z3 can find solutions to more than just SAT problems – it is an SMT solver.

SMT stands for SAT modulo theories; it generalizes SAT to formulas involving integers, strings, arrays, and so on. For example, we can use Z3 to find a solution for the system of equations 3x - 2y = 1, y - x = 1. 


from z3 import *
x, y = Ints('x y')
solve(3 * x - 2 * y == 1, y - x == 1)

# Output: [x = 3, y = 4]

solve is shorthand for the check and model we were using above.

12.3 Solving Puzzles with SMT🔗

SMT solvers are useful for more than finding solutions to a random set of equations – you just have to know how to encode your problem in a form that the SMT solver understands. Here are three examples of puzzles that an SMT solver can solve. Next time you’re working on a puzzle, ask yourself whether it could be solved using SMT.

Often, SMT solvers are not used to find a solution, but to *prove that no solution exists*. For instance, say that we want to prove the mathematical fact y > 0 ==> x + y > x. To do this, we can ask the SMT solver if it ever the case that this is not true.


x, y = Ints('x y')
solve(Not(Implies(y > 0, x + y > x)))

# Output: no solution

The output here says that it is never not the case that y > 0 ==> x + y > x (a double negative). In other words: this formula is true for any choice of x and y!

12.4 Rabbits and Chickens🔗

Uncle Henry has 48 rabbits and chickens. He knows his rabbits and chickens have 108 legs, but does not know the exact number of rabbits and chickens. Can you help him? How many rabbits and chickens does Uncle Henry have?


#Create 2 integer variables
rabbit, chicken = Ints('rabbit chicken')
s = Solver()
s.add(rabbit + chicken == 48) # 48 animals
s.add(4 * rabbit + 2 * chicken == 108) # 108 legs
s.check() # solve the constraints
s.model() # get the solution

12.5 Cats and Dogs🔗

Say that you want to spend exactly 100 dollars to buy exactly 100 animals. Dogs cost 15 dollars, cats cost 1 dollar, and mice cost 25 cents each. You have to buy at least one of each. How many of each should you buy? Solution from


# Create 3 integer variables
dog, cat, mouse = Ints('dog cat mouse')

solve(dog >= 1,                   # at least one dog
      cat >= 1,                   # at least one cat
      mouse >= 1,                 # at least one mouse
      dog + cat + mouse == 100,   # 100 animals total
      # We have 100 dollars (10000 cents):
      #   dogs cost 15 dollars (1500 cents), 
      #   cats cost 1 dollar (100 cents), and 
      #   mice cost 25 cents 
      1500 * dog + 100 * cat + 25 * mouse == 10000)

12.6 Sudoku🔗

Sudoku is a puzzle where the goal is to insert numbers in boxes to satisfy the following condition: each row, column, and 3x3 box must contain the digits 1 through 9 exactly once.

The solution for the puzzle shown below. You can run it with ‘python3 sudoku.py‘.


from z3 import *

# 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
      for i in range(9) ]

# each cell contains a value in {1, ..., 9}
cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9)
             for i in range(9) for j in range(9) ]

# each row contains a digit at most once
rows_c   = [ Distinct(X[i]) for i in range(9) ]

# each column contains a digit at most once
cols_c   = [ Distinct([ X[i][j] for i in range(9) ])
             for j in range(9) ]

# each 3x3 square contains a digit at most once
sq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j]
                        for i in range(3) for j in range(3) ])
             for i0 in range(3) for j0 in range(3) ]

sudoku_c = cells_c + rows_c + cols_c + sq_c

# sudoku instance, we use '0' for empty cells
instance = ((0,0,0,0,9,4,0,3,0),
            (0,0,0,5,1,0,0,0,7),
            (0,8,9,0,0,0,0,4,0),
            (0,0,0,0,0,0,2,0,8),
            (0,6,0,2,0,1,0,5,0),
            (1,0,2,0,0,0,0,0,0),
            (0,7,0,0,0,0,5,2,0),
            (9,0,0,0,6,5,0,0,0),
            (0,4,0,9,7,0,0,0,0))

instance_c = [ If(instance[i][j] == 0,
                  True,
                  X[i][j] == instance[i][j])
               for i in range(9) for j in range(9) ]

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
    m = s.model()
    r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
          for i in range(9) ]
    print_matrix(r)
else:
    print("failed to solve")

12.7 Sum of Two Real Numers🔗

The sum of two nonzero real numbers is 4 times their product. What is the sum of the reciprocals of the two numbers? We’re going to solve this over real numbers: 


from z3 import *
x, y = Reals('x y') 
s=Solver() 
s.add(x > 0)
s.add(y > 0) 
s.add(x + y == 4 * x * y)
print (s.check())
m=s.model()
print ("the model:", m)
print ("the answer:",m.evaluate (1/x + 1/y))
# 1/x + 1/y = (x+y)/ (x * y) == 4
#Instead of pulling values from the model and then 
# compute the final result on Python’s side, 
# we can evaluate an expression ( x1 + y1 ) inside the model we’ve got:
#sat
#the model:
#[x = 1, y = 1/3] 
#the answer: 4

12.8 Coin Sum🔗

Euler 31: “Coin sums” problem is as follows: In the United Kingdom the currency is made up of pound (£) and pence (p). There are eight coins in general circulation: 1p, 2p, 5p, 10p, 20p, 50p, £1 (100p), and £2 (200p). It is possible to make £2 in the following way: 

1×£1 + 1×50p + 2×20p + 1×5p + 1×2p + 3×1p
How many different ways can £2 be made using any number of coins?


from z3 import *
a,b,c,d,e,f,g,h = Ints('a b c d e f g h')
s = Solver()
s.add(1*a + 2*b + 5*c + 10*d + 20*e + 50*f + 100*g + 200*h == 200,
      a>=0, b>=0, c>=0, d>=0, e>=0, f>=0, g>=0, h>=0) 
result =[]
while True:
    if s.check() == sat:
        m = s.model()
        print (m)
        result.append(m)
        # Create a new constraint the blocks the current model 
        block = []
        for d in m:
            # create a constant from declaration
            c=d()
            block.append(c != m[d]) 
        s.add(Or (block))
    else:
        print (len(result))
        break

12.9 8 Queens Puzzle🔗

The 8-Queens problem asks: given an 8×8 chessboard, place 8 queens on the board so that no two queens attack each other.


from z3 import *
N = 8

def var(row, col):
    return Int(f'cell_{row}_{col}')


vs = [ [ var(row, col) for col in range(N) ] for row in range(N) ]
cells_defined = [
      And(0 <= vs[i][j], vs[i][j] <= 1)
      for i in range(N) for j in range(N)
    ]
s = Solver()
s.add(cells_defined)
rows_ok = [Sum(vs[i]) == 1 for i in range(N)]

# all entries within a column must be distinct
cols_ok = [Sum([vs[i][j] for i in range(N)]) == 1 for j in range(N) ]

diagonals_ok = [Implies( And(vs[i][j] == 1, vs[k][h] == 1, 
                i != k, j != h), abs(k - i) != abs(j - h))
    for i in range(N) for j in range(N) 
    for k in range(N) for h in range(N)]

s.add(rows_ok)
s.add(cols_ok)
s.add(diagonals_ok)
if s.check() == sat:
    m = s.model()
    for i in range(N):
        for j in range(N):
            if m[var(i,j)] == 1:
                print(m[var(i,j)],end ="|")
            else:
                print(" ",end ="|")
        print("
---------------")
else:
    print("unsat")

12.10 Circle, Square, and Triangle🔗 


# circle + circle = 10
# circle * square + sqaure = 12
# circle * square - triangle * circle = circle
# What is th evalue of the triangle?

#!/ usr/bin/ python
from z3 import *
circle , square , triangle = Ints('circle square triangle')
s = Solver()
s.add( circle + circle ==10)
s.add( circle * square + square ==12)
s.add( circle *square - triangle * circle == circle )
if s.check() == unsat:
    print("UNSAT")
else:
    print (s.model())

12.11 De Morgan’s laws🔗

We want to prove

We will prove it by showing there is no falsifying interpertation of the formula.


from z3 import *
p, q = Bools('p q')
demorgan = And(p, q) == Not(Or(Not(p), Not(q)))
print (demorgan)

def prove(f):
    s = Solver()
    s.add(Not(f))
    if s.check() == unsat:
        print ("proved")
    else:
        print ("failed to prove")

print ("Proving demorgan...")
prove(demorgan)

12.12 Integer Overflow🔗

When a 16-bit vector is used, any integer greater than 2^16 - 1 = 65,535 will cause BV2Int to overflow. In the example below, if the sum of x and y exceeds 65,535, then BV2Int(x) + BV2Int(y) will not be equal to BV2Int(x + y). 


from z3 import *
x = BitVec('x', 16)
y = BitVec('y', 16)
s = Solver()
s.add((BV2Int(x) + BV2Int(y)) != BV2Int(x+y))
if s.check()== sat:
    print(s.model())
else:
    print("unsat")

solve(BV2Int(x)+1 != BV2Int(x+1))

12.13 Wedding Seating🔗

Encode the placement of wedding guests in Z3.

  • Alice does not sit next to Charlie

  • Alice does not sit on the leftmost chair

  • Bob does not sit to the right of Charlie

  • Each person gets a chair

  • Every person gets at most one chair

  • Every chair gets at most one person

We will model assignment via nine boolean variables xpc, meaning the person p sits in chair c. Here are the constraints:


from z3 import *
xal, xam, xar, xbl, xbm, xbr, xcl, xcm, xcr = 
     Bools('xal xam xar xbl xbm xbr xcl xcm xcr')
s = Solver()
# Alice does not sit next to Charlie
s.add(And(Implies(Or(xal, xar), Not(xcm) ), 
       Implies(xam, And(Not(xcl), Not(xcr)))))
# Alice does not sit on the leftmost chair
s.add(Not(xal) )
# Bob does not sit to the right of Charlie
#s.add(And( Implies(xcl, Not(xbm)), Implies(xcm, Not(xbr))))

#Each person gets a chair
s.add( Or( xal, xam, xar) )
s.add( Or( xbl, xbm, xbr) )
s.add( Or( xcl, xcm, xcr) )

#Every person gets at most one chair
s.add( Or( Not(xal), Not(xam) ) )
s.add( Or( Not(xal), Not(xar) ) )
s.add( Or( Not(xam), Not(xar) ) )

#analogous for persons b and c
s.add( Or( Not(xbl), Not(xbm) ) )
s.add( Or( Not(xbl), Not(xbr) ) )
s.add( Or( Not(xbm), Not(xbr) ) )

s.add( Or( Not(xcl), Not(xcm) ) )
s.add( Or( Not(xcl), Not(xcr) ) )
s.add( Or( Not(xcm), Not(xcr) ) )


# Every chair gets at most one person
s.add( Or( Not(xal), Not(xbl) ) )
s.add( Or( Not(xal), Not(xcl) ) )
s.add( Or( Not(xbl), Not(xcl) ) )
# analogous for chairs m and r

s.add( Or( Not(xam), Not(xbm) ) )
s.add( Or( Not(xam), Not(xcm) ) )
s.add( Or( Not(xbm), Not(xcm) ) )

s.add( Or( Not(xar), Not(xbr) ) )
s.add( Or( Not(xar), Not(xcr) ) )
s.add( Or( Not(xbr), Not(xcr) ) )

if s.check() == sat:
    print(s.model())
else:
    print("UNSAT")

    contents    up