Z3 : Satisfiability Modulo Theory solver
Hi all,
Over the last weeks, maybe months, I'm digging out more and more projects of the RiSE division @ Microsoft.
This division is focused on research projects and generally you discover mind-blowing projects on their site.
Pex was one of them, but in the foundation of Pex, is Z3.
What is Z3 ?( its not only a car ! )
Z3 is a constraint solver that is also known as a SMT (Satisfiability Modulo Theory) solver.
In short, this allows you to define a problem and check wherever it is satisfiable or not.
Assume the following constraint:
a > 0 & a <2
In this very simple case Z3 will tell you that its feasable and that a possible value for a would be 1.
Z3 will not enumerate all the possibilities or optimize any parameter of the formula, it will just check if its feasable or not.
So we can now ask if there would be another solution by setting the constraint to :
a > 0 & a < 2 & a != 1
Now Z3 will tell us that our constraint is not satisfiable anymore and will not return any value.
So far for the theory: Z3 solves arithmetically expressed problems.
Z3 is not .Net, but it has a .Net Api, its not even based on the (CTS) Common Type System, and thus uses very own types.
That type System does not include the .Net types and is rather limited, as a counterpart it provides room for much bigger numbers than the typical int and long types of .Net even decimal an float have no real limits.
This would allow you to define a 128bit signed or not integer.
The problem remains in the translation, how do we translate all the binary operations as =, !=, <, >, &&, ||, ... to Z3 Terms and Constraints.
Z3 allows also defining Tuples, DataTypes to model your problem but you need to translate them from very low level (char, int, bool) to complex classes with multiple fields or various mixed types. A string could be an array of unsigned 8 bit vector for example.
LinqToZ3
Bart De Smet is a brilliant developer that was kidnapped from our dear Belgium by the Redmond boys and is now working on our future compilers and framework versions.Bart took a look to Z3 and translated Linq Expressions as "Where( a=> a.X > 0 && a.X < 2)" to Z3 constraints, that have a less readable form as (and(> (x,0)),(<(x,2))).
There is a great series of posts about his work, there is still no code available from an official source, but I was able to build it from its explanations and with some modifications to the new version of Z3.
Later I spend a bit time to play around with it and map other types and test a bit.
If you want the code to test it out, give me a sign.
Thanks to the Linq approach we are able to express Theorems as Linq Expressions, these expressions also referred as Monads, are just there to model the constraints.
When you write the following Linq Expression in a LinqToSql context for example:
var entities = data.Where(a=> a.Title == "Test");
The part (a=> a.Title == "Test") is sent to the LinqProvider that will translate that so Sql language as :
'select * from table where Title = "Test"'.
The Sql statement gets executed but not the linq expression it’s just a description of the statement.
When you have this in place LinqToZ3 is then able to make the translation of your types to Z3 types and the constraints are mapped to Z3 constraints. Because Z3 supports all the typical binary operators this is not really difficult to do.
Now we can start making some more complex rules and combine any number of binary branches and operations, +, -, *, /, mod, etc.
You can write quite complex problem solving programs without writing a real line of the algorithm implementation. You just need to define the rules of your problem.
Sudoku Solver
The most interesting sample I found of this is probably the Sudoku Solver.
Imagine how you would write it :
A couple of loops, a lot of backtracking, maybe solving multiple possibilities at a time, etc.
Sounds not like a 5 minute job...
Now with Z3 it’s much easier:
Tell to Z3 that:
- Any cell can contain any number from 1 to 9. | Where (a => a.Cell1 => 1 && a.Cell1 =< 9)
- All cells on a row or column must be distinct values. | Where (a => Distinct(Cell1,...))
- 3by3 groups can contain any number from 1 to 9 only once. | Where (a => Distinct(Cell1,...))
- Now tell Z3 the cells you are sure of Cell3 = 1, Cell5 = 8 | Where (a => a.Cell3 == 1, ....)
Now sit back and wait a couple of seconds and let the magic happen.
The code that Bart uses is based on Integer types within Z3 and these are much less performing in this case than when using Bit Vectors.
Using Bit Vectors it becomes a matter of milliseconds to solve the puzzle.
Other applications
Other applications are various and expanding every day.
Z3 is often used by code analysis tools like in : CodeContracts, Pex, and others.
The usage there is : give me, or are their any arguments that will satisfy a couple of constraints.
Pex for example guesses arguments that will make the code enter in particular branches to have the biggest code coverage possible.
CodeContracts analyses if all the possible error cases are covered in the code.
For example if you have a method that takes an int as parameter.
And in your method you use that parameter for accessing items within an array.
CodeContracts will warn you that there is a possible OutOfRange exception.
I you add a check and throw your own exception, the warning will disappear, because it cannot find an argument that will break the code.
I don’t really remember if code contracts are based on Z3, but it’s using SMT somehow.
After the first releases of Z3 a lot of tools appeared, either using Z3 either built on the elements composed by it.
Z3 was a big breakthrough at RiSE and will for sure be the animator or build stone for other projects. See RiSE4fun.
That was it !
Hope you enjoyed, next post will be over Z3's big brother: Microsoft Solver Foundation.