Microsoft Z320. Jan '14

Introduction

Z3 is a high-performance theorem proved depeloped at Microsoft. It is distributed under Microsoft Research License Agreement which means it is open-source, free for educational and personal use. For commercial purposes a license has to be purchased which makes this project technically not Free Software.

Z3 is written in C++ but has bindings for .NET, Python and Ocaml. The bindings make it possible to manipulate Z3 data structures directly and efficiently. Microsoft Z3 also supports theories written using SMT-LIB notation which is quite different from traditional programming languages.

SMT-LIB notation

Z3 can be invoked to parse SMT-LIB files with -smt2 flag, it is also possible to read commands from standard input in which case Z3 behaves pretty much like a shell for SMT-LIB statements:

z3 -smt2 -in

Defining variables is done by defining a function that has no arguments, in this case we're defining x:

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)

Defining functions is done similarily, for instance function named f which accepts one integer argument and returns an integer argument:

(declare-fun f (Int) Int)

Of function named g which accepts two integers and returns integer:

(declare-fun g (Int Int) Int)

Adding constraints to build up the theory for Z3 is done with assert keyword. Mathematical formulas are written using prefix notation, thus formula like:

\begin{equation*} 2 * x >= y + z \end{equation*}

Becomes:

(assert (>= (* 2 x) (+ y z)

What is unique about Z3 as with most SMT-s is that uninterpreted functions can be defined:

(assert (< (f x) (g x x)))
(assert (> (f y) (g x x)))

To check the satifiability of the formulas a check-sat statement is issued:

(check-sat)

Which will return sat or unsat depending on whether the conditions are satisfied or not.

Python bindings

Converting a problem to SMT-LIB format might be time-consuming and error-prone so Z3 tries to integrate well with already existing programming languages and frameworks. In most examples all Z3 classes are loaded to local namepsace:

from z3 import *

Defining variables for Z3 means instantiating a Int or Real class from z3 module, the argument for the class constructor is the variable name for z3:

x = Int("x")
y = Int("y")
z = Int("z")

In case of Python there is no global theory state, thus all variables constraints and formulas have to be bound to a a solver instance:

s = Solver()

Since Python supports operator overloading the formula definitions become much more readable for an regular programmer:

s.add(2*x >= y + z)

To check whether the theory holds:

s.check()

Solving sudoku with Z3

Using Z3 to solve sudoku is quite straightforward if you understand the basic concepts of declarative programming and have familiarised yourself with the operands that Z3 implements. In this case we are using <= (less than or equal), >= (greater than or equal), And, Distinct operands to form the theory using Z3.

import sys
import itertools
from z3 import *

# Create solver
s = Solver()

# Create Z3 integer variables for matrix cells
cells = [ [ Int("z_%s_%s" % (i+1, j+1)) for j in range(9) ] for i in range(9) ]

# Add sudoku problem instance constraints
for y, line in enumerate(open(sys.argv[1], "rU").read().split("\n")):
    for x, value in enumerate(line):
        if value != ".":
            s.add(cells[x][y] == value)

# Add cell constraints
for y in range(9):
    for x in range(9):
        s.add(And(1 <= cells[x][y], cells[x][y] <= 9))

# Add column constraints
for x in range(9):
    s.add(Distinct(cells[x]))

# Add row constraints
for y in range(9):
    s.add(Distinct([cells[x][y] for x in range(9)]))

# Add group constraints
for y in range(0,9,3):
    for x in range(0,9,3):
        s.add(Distinct([cells[x+i][y+j] for i, j in itertools.product(range(3), range(3))]))

# Check if constraints have been satisfied
if s.check() == sat:
    m = s.model()
    for y in range(9):
        print "".join([str(m.evaluate(cells[x][y])) for x in range(9) ])
else:
    print "Failed to solve"

As an input file we use in53.pzl:

.27.3....
1......7.
.83.7.24.
.71..5...
.3.....8.
...9..12.
.15.2.49.
.4......8
....1.56.

Running the script presented earlier:

python solve_using_z3.py in53.pzl

Yields in following output:

Generating SMT-LIB notation

To generate widely recognized SMT-LIB notation of the theory we can use similar approach, only syntax differs:

"""
Piece of code to convert Sudoku problem files to SMT2 theories
"""

import sys

print "(set-info :source | Python ftw |)"

print "; Declare variables"
for y in range(9):
    for x in range(9):
        print "(declare-fun z_%d_%d () Int)" % (x,y)

print "; Sudoku problem instance constraints:"
for y, line in enumerate(open(sys.argv[1], "rU").read().split("\n")):
    if not line: break
    print ";", line
    for x, value in enumerate(line):
        if value != ".":
            print "(assert (= z_%d_%d %s))" % (x,y,value)

print "; Cell constraints"
for y in range(9):
    for x in range(9):
        print "(assert (and (< 0 z_%d_%d) (> 10 z_%d_%d)))" % (x,y,x,y)

print "; Column constraints"
for x in range(9):
    print "(assert (distinct",
    for y in range(9):
        print "z_%d_%d" % (x,y),
    print "))"

print "; Row constraints"
for y in range(9):
    print "(assert (distinct",
    for x in range(9):
        print "z_%d_%d" % (x,y),
    print "))"

print "; Group constraints"
for y in range(0,9,3):
    for x in range(0,9,3):
        print "(assert (distinct",
        for i in range(3):
            for j in range(3):
                print "z_%d_%d" % (x+i,y+j),
        print "))"

print
print "; Check satisfiability"
print "(check-sat)"
print "(get-model)"

Theory generated by this code can be viewed and proven here.

Links

SMT Z3 TU Berlin QAoES SAT