Programming Constraint Services with Z3

DPLL [20]

CDCL: Modern Search [50]

• Efficient indexing (two-watch literal)

• Non-chronological backtracking (backjumping)

• Lemma learning

• Variable and phase selection

• Garbage collection, restarts

CDCL: State [45]

• : Atomic predicates

• : Literals over atoms

• : Partial assignment without complementary literals.

• : A clause - disjunction of literals.

• : a decision literal.

• : a literal with explanation clause , where is a disjunct in . The literal is assigned relative to partial assignment when all other literals in occur negatively in .

• : A set of clauses.

CDCL: Formal System [6]

CDCL(T)

CDCL(T) Example

Models and Proofs

CDCL realizes the dichotomy by interleaving model and consequence finding:

Realizing the dichotomy

Main invariants preserved by CDCL:

• Conflict state: For the state it is the case that and .

• Propagation: For the state and , whenever , then and .

Illustrating the invariants

if

• Finds First Unique Implication Point (FUIP)
  • minimizes number of decision literals in .
  • maximizes propagated literals in

Equality and Uninterpreted functions

EUF

  (declare-sort A)
  (declare-fun f (A) A)
  (declare-const x A)
  (assert (= (f (f x)) x))
  (assert (= (f (f (f x))) x))
  (check-sat)
  
  (assert (not (= (f x) x)))
  (check-sat)

Deciding Equality

Disequalities

Variants of union-find are effective to decide equality.

Free functions

Congruence rule

Naming sub-terms

Applying Congruence (1)

Applying Congruence (2)

EUF Models

A satisfiable version:

EUF Models (II)

• Associate a distinct value with each equivalence class.

Linear Arithmetic

Linear Arithmetic Example

(set-logic QF_IDL) ; optional in Z3
(declare-fun t11 () Int)
(declare-fun t12 () Int)
(declare-fun t21 () Int)
(declare-fun t22 () Int)
(declare-fun t31 () Int)
(declare-fun t32 () Int)

(assert (and (>= t11 0) (>= t12 (+ t11 2)) (<= (+ t12 1) 8)))
(assert (and (>= t21 0) (>= t22 (+ t21 3)) (<= (+ t22 1) 8)))
(assert (and (>= t31 0) (>= t32 (+ t31 2)) (<= (+ t32 3) 8)))
(assert (or (>= t11 (+ t21 3)) (>= t21 (+ t11 2))))
(assert (or (>= t11 (+ t31 2)) (>= t31 (+ t11 2))))
(assert (or (>= t21 (+ t31 2)) (>= t31 (+ t21 3))))
(assert (or (>= t12 (+ t22 1)) (>= t22 (+ t12 1))))
(assert (or (>= t12 (+ t32 3)) (>= t32 (+ t12 1))))
(assert (or (>= t22 (+ t32 3)) (>= t32 (+ t22 1))))
(check-sat)
(get-model) ; display the model  

Algorithmic Fragments of Arithmetic

Other Fragments of Arithmetic

• NIA - There is no decision procedure for integer polynomial constraints

  • Z3 falls back to incomplete heuristics
  • NIA over bounded integers may get translated to bit-vector constraints

  
  Theories, where Z3 falls back to general solvers:

• Bi-linear real arithmetic

• Non-unit two-variable per inequality

• At most one unit positive variable per inequality (Horn)

Bellman-Ford

Solve difference logic using graph Bellman-Ford network flow algorithm. Negative cycle unsat.

General form Simplex [21]

General form and

Only bounds (e.g., ) are asserted during search.

From Definitions to a Tableau

- are basic (dependent)
- are non-basic

Pivoting

• Value of non-basic variable can be chosen between and .
• Value of basic variable is a function of non-basic variable values.
• Pivoting swaps basic and non-basic variables.
  • used to get values of basic variables within bounds.

Arrays

Arrays

; This example illustrates different uses of the arrays
; supported in Z3.
; This includes Combinatory Array Logic 
; (de Moura & Bjorner, FMCAD 2009).
;
(define-sort A () (Array Int Int))
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(declare-fun a1 () A)
(declare-fun a2 () A)
(declare-fun a3 () A)
(push) ; illustrate select-store
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(check-sat)
(get-model)
(assert (not (= x y)))
(check-sat)
(pop)
(define-fun all1_array () A ((as const A) 1))
(simplify (select all1_array x))
(define-sort IntSet () (Array Int Bool))
(declare-fun a () IntSet)
(declare-fun b () IntSet)
(declare-fun c () IntSet)
(push) ; illustrate map
(assert (not (= ((_ map and) a b) ((_ map not) ((_ map or) ((_ map not) b) ((_ map not) a))))))
(check-sat)
(pop)
(push) 
(assert (and (select ((_ map and) a b) x) (not (select a x))))
(check-sat)
(pop)
(push) 
(assert (and (select ((_ map or) a b) x) (not (select a x))))
(check-sat)
(get-model)
(assert (and (not (select b x))))
(check-sat)
;; unsat, so there is no model.
(pop)  
(push) ; illustrate default
(assert (= (default a1) 1))
(assert (not (= a1 ((as const A) 1))))  
(check-sat)
(get-model)
(assert (= (default a2) 1))
(assert (not (= a1 a2)))
(check-sat)
(get-model)
(pop)
(exit)    

Arrays as Combinators [42]

  A = Array(Index, Elem) # array sort 
  
  a[i]             # index array 'a' at index 'i'
                   # Select(a, i)
  
  Store(a, i, v)   # update array 'a' with value 'v' at index 'i'
                   # = lambda j: If(i == j, v, a[j])
    
  Const(v, A)      # constant array
                   # = lambda j: v
  
  Map(f, a)        # map function 'f' on values of 'a'
                   # = lambda j: f(a[j])

  Ext(a, b)        # Extensionality
                   # Implies(a[Ext(a, b)] == b[Ext(a, b)], a == b)

Array Decision Procedure

Example Store(a, i, v)

• Each occurrence of Store(a, i, v) and b[j],

  • Assert Store(a, i, v)[j] == If(i == j, v, a[j])
  • Assert Store(a, i, v)[i] == v

• Each shared occurrences of :

  • Assert .

• Suppose we are given a model satisfying all asserted equalities.

  • assigns values to terms.
  • Extend: .
  • Claim: satisfies Store axioms.

Efficient Array Decision Procedures

• Use current partial interpretation to guide axiom instantiation.

• Rough sketch:

  • If (congruent) in current state
    • Assert .
  • If in current state
    • Assert

• Also important to limit set of pairs.

  • Z3 uses relevancy propagation to prune don't care literals
  • Boolector uses dual propagation to extract small implicant

Bit-Vectors

Bit-Vectors

(define-fun is-power-of-two ((x (_ BitVec 4))) Bool 
  (= #x0 (bvand x (bvsub x #x1))))
(declare-const a (_ BitVec 4))
(assert 
 (not (= (is-power-of-two a) 
         (or (= a #x0) 
             (= a #x1) 
             (= a #x2) 
             (= a #x4) 
             (= a #x8)))))
(check-sat)

Floating Points

Floating point example

(declare-fun X () (_ FloatingPoint 11 53))

(assert (fp.isNormal X))
(assert (not (fp.isSubnormal X)))
(assert (not (fp.isZero X)))
(assert (not (fp.isInfinite X)))
(assert (not (fp.isNaN X)))
(assert (not (fp.isNegative X)))
(assert (fp.isPositive X))

(check-sat)
(get-model)

Sequences and Strings

Sequence Example

(declare-const a String)
(declare-const b String)
(declare-const c String)
(assert (str.prefixof b a))
(assert (str.suffixof c a))
(assert (= (str.len a) (+ (str.len b) (str.len c))))
(assert (not (= a (str.++ b c))))
(check-sat)  

Queues

Non-linear Arithmetic

Decision Procedure Highlight [30]

QSAT

The idea by example

• : starts. is false.
• : strikes back. is true.
• : has to backtrack. is already forced true.
• : learns .
• : is false.
• : counters - is true.
• : has yet again to consider if it can change its guess for . But is already unsatisfiable. The universal player has to give up and the existential player established that the formula is true.

Summary of approach

• Two players try to find values

  • - to satisfy
  • - to satisfy

• Players control their variables

  • at round :
    • value of is already fixed,
    • fixes value of ,
    • fixes value of , but can change again it at round ,
    • can guess values of of to satisfy .

• Some play loses at round .

  • Create succinct no-good to strengthen resp. .
  • Backjump to round (or below).

Finding small good no-goods

• Player has lost at round

  • Player found a model at round , .

  • induces an evaluation on a subset of literals in , such that .

  • is an unsatisfiable core for .

• Model Based Projection

  • Find a , such that Any .

    • should be weak.
    • should be cheap to find.

  • Then can block .

  • Idea: Use to find a sufficient .

Model-based Projection

   def sign(M,a): if M(a) return a else return a

Model-based Projection for LRA

Model-based Projection for LIA

Model-based Projection for Term Algebras - Sketch

Model-based projection for NRA

• Theory: Non-linear polynomial arithmetic

• Partial CAD - model-based projection [30]

  • Given model , such that
  • Find , such that
    • is valid

• CAD decomposes into sign-invariant cylinders.

• Choose the cylinder where is a member.

Model-based projections, two lenses

Sat based MBP:

• Given:

• Find: , free for

• Such that:

Contrast this with Core-based MBP:

• Given: .

• Find: , free for

• Such that:

Claim: the two compute the same solutions if the projection operators are independent of the value of .

Initialization

   def level(j,a): return max level of bound variable in atom a of parity j     

Property Directed QSAT Algorithm

  def strategy(M,j): return 
  def tailv(j): return 
    
  j = 1
  M = null
  while True:
    if  strategy(M, j) is unsat:
      if j == 1: 
        return F is unsat
      if j == 2:
        return F is sat
      C = Core(, strategy(M, j))
      J = Mbp(tailv(j), C)
      j = index of max variable in J  of same parity as j      
       = J
      M = null
    else:
      M = current model
      j = j + 1 
         

Finding strategies

• Other main ingredient of QSAT is option for players to narrow options of opponents by revealing a strategy

  • at round :
    • value of is already fixed,
    • fixes value of ,
    • can make a function of .

• Developing practical strategies is work in progress

  • For QBF can use Q-resolution proofs as guide [10]

Programmatic Interface

s = Solver()


s.add()
s.assert_and_track()

s.push()
s.pop()

s.check()
s.check()

s.model()
s.proof()
s.unsat_core()   

s.statistics()     

Assertions

s.add()
s.assert_and_track()

Scopes

s.push()

s.pop()

Check Satisfiability

s.check()

s.check()

Certificates

s.model()

s.proof()

s.unsat_core()   

Cores, Correction Sets, Satisfying Assignments

• (M)US (Minimal) unsatisfiable subset

  • (minimal) subset of assertions that are unsatisfiable. Also known as a core

• (M)SS (Maximal) satisfiable subset

  • (maximal) subset of assertions that are satisfiable.

• (M)CS (Minimal) correction set

  • complement of an (M)SS.

• (Prime) implicant

  • iff is a core for .

A Duality: MUS MCS [49]

All Cores and Correction Sets [34]

def ff(s, p): 
    return is_false(s.model().eval(p))

def marco(s, ps):
    map = Solver()
    while map.check() == sat:
        seed = {p for p in ps if not ff(map, p)}
        if s.check(seed) == sat:
           mss = get_mss(s, seed, ps)
           map.add(Or(ps - mss))
           yield "MSS", mss
        else:
           mus = get_mus(s, seed)
           map.add(Not(And(mus)))
           yield "MUS", mus

Maximizing Satisfying Assignments [39]

def tt(s, f): 
    return is_true(s.model().eval(f))

def get_mss(s, mss, ps):
    ps = ps - mss
    backbones = set([])
    while len(ps) > 0:
       p = ps.pop()
       if sat == s.check(mss | backbones | { p }):
          mss = mss | { p } | { q for q in ps if tt(s, q) }
          ps  = ps - mss
       else:
          backbones = backbones | { Not(p) }
    return mss
          

Minimizing Cores [2, 15, 31, 36]

Use built-in core minimization:

s.set("sat.core.minimize","true")  # For Bit-vector theories
s.set("smt.core.minimize","true")  # For general SMT 

Or roll your own:

def quick_explain(s, mus):
    return qx(s, mus, set([]), False)

def qx(s, mus, S, has_support):
    if has_support:
       if s.check(S) == unsat:
          return set([]), { l for l in s.unsat_core() }
    if len(mus) == 1:
       return S, mus    
    mus1, mus2 = split(mus)
    mus2, S = qx(s, mus2, S | mus1, {} != mus1)
    mus1 = S & mus1
    mus2, S = qx(s, mus1, S | mus2 - mus1, {} != mus2)
    return S & mus, S - mus2
    
def split(S1):
    S1, S2 = S1.copy(), set([])
    for i in range(len(S1)/2):
        S2 |= { S1.pop() }
    return S1, S2

s = Solver()
a, b, c, d, e = Bools('a b c d e')
s.add(Or(a, b))
s.add(Or(Not(a), Not(b)))
s.add(Or(b, c))
s.add(Or(Not(c), Not(a)))

print s.check([a,b,c,d,e])
print s.unsat_core()

mus, S = quick_explain(s, {a,b,c,d})

All maximal satisfying sets (basic)

def all_mss(s, ps):
    while sat == s.check():
        mss = get_mss(s, { p for p in ps if tt(s, p) }, ps)
        s.add(Or(ps - mss))
        yield "MSS", mss

• Inefficiency: Same unsat cores may be revisited.

All Correction Sets

Find all satisfying subsets among :

• Initialize: , .
• While is sat:
  • If is sat with model
    • is mss.
    • add mcs
  • Else suppose is a core
    • Replace by :
    • , ,
      , .