Microsoft Z320. Jan '14
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.
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:
(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:
Which will return sat or unsat depending on whether the conditions are satisfied or not.
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:
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, "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:
927431856 164852379 583679241 871265934 239147685 456983127 615728493 342596718 798314562
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, "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.