logicz3smtsat

Combine boolean and integer logic in linear arithmetic using the Z3 Solver?

I would like to solve problems combining boolean and integer logic in linear arithmetic with a SAT/SMT solver. At first glance, Z3 seems promising.

First of all, is it at all possible to solve the following problem? This answer makes it seem like it works.

int x,y,z
boolean a,b,c

( (3x + y - 2z >= 10) OR (A AND (NOT B OR C)) OR ((A == C) AND (x + y >= 5)) )

If so, how does Z3 solve this kind of problem in theory and is there any documentation about it? I could think of two ways to solve this problem. One would be to convert the Boolean operations into a linear integer expression. Another solution I read about is to use the Nelson-Oppen Combination Method described in [Kro 08].

I found a corresponding documentation in chapter 3.2.2. Solving Arithmetical Fragments, Table 1 a listing of the implemented algorithms for a certain logic.

Solution

  • Yes, SMT solvers are quite good at solving problems of this sort. Your problem can be expressed using z3's Python interface like this:

    from z3 import *

x, y, z = Ints('x y z')
A, B, C = Bools('A B C')

solve (Or(3*x + y - 2*z >= 10
      ,  And(A, Or(Not(B), C))
      ,  And(A == C, x + y >= 5)))

    This prints:

    [A = True, z = 3, y = 0, B = True, C = True, x = 5]

    giving you a (not necessarily "the") model that satisfies your constraints.

    SMT solvers can deal with integers, machine words (i.e., bit-vectors), reals, along with many other data types, and there are efficient procedures for combinations of linear-integer-arithmetic, booleans, uninterpreted-functions, bit-vectors amongst many others.

    See http://smtlib.cs.uiowa.edu for many resources on SMT solving, including references to other work. Any given solver (i.e., z3, yices, cvc etc.) will be a collection of various algorithms, heuristics and tactics. It's hard to compare them directly as each shine in their own way for certain sublogics, but for the base set of linear-integer arithmetic, booleans, and bit-vectors, they should all perform fairly well. Looks like you already found some good references, so you can do further reading as necessary; though for most end users it's neither necessary nor that important to know how an SMT solver internally works.