Quantified Satisfiability Modulo Theories

E-matching and Pattern based quantifier instantiation [27]

• • Smallest subterm containing :
  • Use ground equality to match with .

• Formulas are ground unsatisfiable.

E-matching - efficiency

• Secret sauce is to find instantiations
  • quickly,
  • across large sets of terms, and
  • incrementally.

E-matching - basic algorithm

Takes

• a ground term,
• a pattern that may contain variables, and
• a congruence closure structre cc that for each ground term represents an equivalence class of terms that are congruet in the current context.

E-matching - a primer on congruence closure

• Let be a set of terms and set of equalities over .

• A congruence closure over modulo is the finest a partition of , cc, such that:

  • if , then are in the same partition in cc.

  • for ,

    • if are in same partition of cc for each , then
    • are in the same partition under cc.

  • Convention: , maps term to its equivalence class.

E-matching - basic algorithm, code

def match(pattern, term, , cc):
    pattern = pattern
    if pattern == term:
       yield 
    elif is_var(pattern):
       yield pattern term
    else:
       f(patterns) = pattern
       for f(terms) in cc(term):  
          # e.g., with same head function symbol f
          for  in matches(patterns, terms, , cc):
            yield 

def matches(patterns, terms, , cc):
    if not patterns:
       yield 
       return
    for  in match(patterns[0], terms[0], , cc):
        for  in matches(patterns[1:], terms[1:], , cc):
            yield 

E-matching - basic algorithm, equational form

E-matching - beyond the basic algorithm

• Match is invoked for every pattern in database.
• To avoid common work:
  • Compile set of patterns into instructions.
    • By partial evaluation of naive algorithm
  • Instruction sequences share common sub-terms.
  • Substitutions are stored in registers,
    backtracking just updates the registers.

E-matching - code trees (0)

E-matching - code trees (1)

E-matching - code trees (2)

E-matching abstract machine

E-matching abstract machine - NB

• Patterns that share common (top-down) term structure can share code sequences.

  • This saves on common work.

  • Use the choice instruction to branch when patterns end up having different sub-terms.

• Other instructions are possible,

  • forward pruning: lookahead multiple function symbols in immediate subterms before diving into any subterm.

  • to deal with multi-patterns, when maching more than one pattern at a time.

Inverted path indexing

• During search, congruence classes are merged.

• Q: Which merges could enable pattern to be matched?

• A: When pattern contains term , and

  • a node is in in the same class as a node labeled by ,

  • a node is an argument of in the same position as ,

  • , are merged

• Idea: Build an index of all pairs from patterns.

  • during a merge with look for matches in index.

Model-based Quantifier Instantiation [5, 11, 29, 36]

Check

while is SAT with model :
   if is UNSAT return SAT
   model for
   find , such that .
  
return UNSAT

where is partially evaluated using interpretation .

Partial model evaluation

• is partially evaluated using interpretation .

Example:

Model-based Quantifier Instantiation - scope

Quite powerful when search space for instantiation terms is finite

• EPR, UFBV, Array property fragment, Essentially UF
• Combine with template space
• See also CEGIS

EPR

Also known as Bernays-Schoenfinkel-Ramsey class.

Same complexity as DQBF.

EPR Example

(declare-sort T) 

(declare-fun subtype (T T) Bool)

;; subtype is reflexive
(assert (forall ((x T)) (subtype x x)))

;; subtype is antisymmetric
(assert (forall ((x T) (y T))  (=> (and (subtype x y) (subtype y x)) (= x y))))

;; subtype is transitive
; ...

;; subtype has the tree-property
(assert (forall ((x T) (y T) (z T)) 
  (=> (and (subtype x z) (subtype y z)) (or (subtype x y) (subtype y x)))))

;; we have an additional axiom: every type is a subtype of obj-type
(declare-const obj-type T) ....
(assert (forall ((x T)) (subtype x obj-type)))

(assert (subtype int-type real-type))
(assert (subtype real-type complex-type))
(assert (not (subtype string-type real-type)))

EPR Example - online

EPR decidability

• Skolemize
  • , the are free constants
• Instantiate
  • where ranges over all bindings of to .
• Check ground SAT
• Ground SAT implies finite model of size at most .

EPR using MBQI

• Skolemize

  • , the are free constants

• Models for bind variables to free constants

• The number of possible such models is bounded by .

UFBV [36]

UFBV Example

(set-option :smt.mbqi true)
(define-sort Char () (_ BitVec 8))

(declare-fun f  (Char) Char)
(declare-fun f1 (Char) Char)
(declare-const a Char)

(assert (bvugt a #x00))
(assert (= (f1 (bvadd a #x01)) #x00))
(assert (forall ((x Char)) (or (= x (bvadd a #x01)) (= (f1 x) (f x)))))

(check-sat)
(get-model)

UFBV Example - Online

UFBV decidability

• All variables range over finite domains.

• Quantifier-free fragment is not only NP hard, it is NEXPTIME hard.

  • QF-UFBV can be encoded into EPR. [35]

• Quantified fragment is another complexity jump.

• BV - quantifier elimination [17–19]

• UFBV using MBQI [36]

  • Use templates to find general instances

Map Property Fragment [7]

Map Property Fragment - Example

• is equal to except at index .

• can only have two values, or .

Array Property Fragment [7]

Array Property Example

(set-option :smt.mbqi true)
(set-option :model.compact true)

;; A0, A1, A2, A3, A4 are "arrays" from Integers to Integers.
(declare-fun A0 (Int) Int) (declare-fun A1 (Int) Int)
(declare-fun A2 (Int) Int) (declare-fun A3 (Int) Int)
(declare-fun A4 (Int) Int) 
(declare-const n Int) (declare-const l Int)
(declare-const k Int) (declare-const x Int)
(declare-const y Int) (declare-const w Int)
(declare-const z Int)

;; A1 = A0[k <- w]
(assert (= (A1 k) w))
(assert (forall ((x Int)) (or (= x k) (= (A1 x) (A0 x)))))

;; A2 = A1[l <- x] = A0[k <- w][l <- x]
(assert (= (A2 l) x))
(assert (forall ((x Int)) (or (= x l) (= (A2 x) (A1 x)))))

;; A3 = A0[k <- y]
(assert (= (A3 k) y))
(assert (forall ((x Int)) (or (= x k) (= (A3 x) (A0 x)))))

;; A4 = A3[l <- z] = A0[k <- y][l <- z] 
(assert (= (A3 l) z))
(assert (forall ((x Int)) (or (= x l) (= (A4 x) (A3 x)))))

(assert (and (< w x) (< x y) (< y z)))
(assert (and (< 0 k) (< k l) (< l n)))
(assert (> (- l k) 1))

;; A2 is sorted in the interval [0,n-1]
(assert (forall ((i Int) (j Int))
                (=> (and (<= 0 i) (<= i j) (<= j (- n 1)))
                    (<= (A2 i) (A2 j)))))

(check-sat)
(get-model)

;; A4 is sorted in the interval [0,n-1]
(assert (forall ((i Int) (j Int))
                (=> (and (<= 0 i) (<= i j) (<= j (- n 1)))
                    (<= (A4 i) (A4 j)))))

(check-sat)

Array Property Example - Online

Array property Fragment - sufficient instantiations

• Given formula with free.

• Let be set of a set of from .

• In other words, for every possible instantiation of there is a that satisfies at least the same combination of guards.

Array Property Fragment - arithmetic

Essentially Uninterpreted Fragment [11]

Synthesize generalized instantiation sets using grammar rules.

Applies to winder range of formulas than the syntactic array property fragment.

• list property fragment by McPeak and Necula
• several locally finite theories - Stokkermans et. al.

Essentially Uninterpreted Example

(set-option :smt.mbqi true)
;; f an g are "streams"
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)

;; the segment [a, n + a] of stream f is equal to the segment [0, n] of stream g.
(declare-const n Int)
(declare-const a Int)
(assert (forall ((x Int)) (=> (and (<= 0 x) (<= x n))
                              (= (f (+ x a)) (g x)))))

;; adding some constraints to a
(assert (> a 10))
(assert (>= (f a) 2))
(assert (<= (g 3) (- 10)))

(check-sat)
(get-model)

Essentially Uninterpreted Example - Online

Instantiation sets and Quantifiers

• As pursued in [34]

• The notion of instantiation set can be extended along a different dimension of virtual substitutions.

• Several theories admit quantifier elimination by virtual substitutions.

• Example .

• Tricky part: ensure that set of virtual substitutions does not grow unbounded.

QSAT [2]

Instantiations from repeated SMT calls [25]

Goal: To find a quantifier free , such that

Tool: project that eliminates from a conjunction
         that is, project() .

Initialize:

Repeatedly: find conjunctions that imply

Update: project().

Instantiations - Algorithm

def qe():                   
    e, a = Solver(), Solver()
    e.add()                        
    a.add()
     = False
    while sat == e.check():
        = e.model()
        =   # assume  is in negation normal form
       assert unsat == a.check() 
        = a.unsat_core()
        = project(, )
        = 
       e.add()
    return 

From SMT to QBF and back

• The approach we illustrated was used by Monniaux'08 [25].
  
  

• QESTO [16] generalizes to nested QBF.
  
  

• We generalize QESTO to SMT; improving [25, 26, 31]

Example game [16]

• : starts. .
• : strikes back. .
• : has to backtrack. Already .
• : learns .
• : .
• : counters - .
• : has lost!. Already .

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 player loses at round .

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

Main ingredients: Projection and Strategies

• Projections are added to learn from mistakes.

  • Player avoids repeating same losing moves.
    
    

• Strategies prune moves from opponent.

  • Prevent opponent player from moves.

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 .

    • should be weak, so is a strong blocker.
    • should be cheap to find and avoid space overhead.

  • Then can block .

  • Idea: Use to find a sufficient .

Initialization

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

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 
         

Projection and Strategies

• Projections learn from mistakes, avoids similar mistakes in future rounds.
  
  

• Strategies prune moves from opponent.

Model-based projection - Example

• Want to compute small .

• Note

• Say

• So

Model-based Projection for LRA

Eliminate from conjunction of literals :

Trick: Use to turn into .

Model-based Projection for LRA - resolution

Can now assume occurs only as upper or lower bounds:

Model-based Projection on formulas

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

Model-based Projection for LIA

For LIA, cannot just assume equalities are of the form or . Generally, has a coefficient, that we cannot remove.

Example: .

• What could go wrong if we just reduce to ?
  
  

• Suppose , . So .
  
  

• Cross-multiplying gives , which is feasible, but is infeasible.

Model-based Projection for LIA - integer resolution

Solution: Combine inequalities using resolution

Model-based Projection for LIA - resolution [33]

•   if
  
  

• 
  else if
  
  

• 
  otherwise,
  
  

• satisfies , and …

Model-based Projection for LIA - divisiblity

Resolution introduced divisibility constraints.

So now we also have to eliminate under divisions.

where

• ,

Model-based Projection for Term Algebras

S-expressions: A generic term algebra

• An s-expression is either a nil or a cons.
  
  

• Access arguments of cons using car and cdr.
  
  

• Test terms using cons?(), or nil?()

Model-based Projection for Term Algebras -

amounts to unification

Model-based Projection for Term Algebras -

Case for is symmetric.

Since there is an infinite number of cons-terms.

Model-based projection Term Algebras - adequacy

• New terms are created during
  
  

• but they are of the form following shape of original constructor terms.
  
  

• and they occur in conjunctions with .
  
  

• so produces finite set of projections.

Model-based projection for NRA

• Theory: Non-linear polynomial arithmetic

• Partial CAD - model-based projection [20]

  • 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 [22]:

• Given:

• Find: , free for

• Such that:

Contrast this with Core-based MBP [30]:

• Given: .

• Find: , free for

• Such that:

Claim: (Roughly) The same projection operator can be used in both cases if occurs in all literals and the operator is stable under changes to the value of .

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 [3]

  • Method by Markus Rabe can be seen as a strategy.

Horn Clauses [12–14, 24]

def mc(x):
    if x > 100:
       return x - 10
    else:
       return mc(mc(x + 11))

def contract(x):
    assert(x > 101 or mc(x) == 91)

   (set-logic HORN)
   (declare-fun mc (Int Int) Bool)
   (assert 
     (forall ((x Int)) 
          (=> (> x 100) 
              (mc x (- x 10)))))
   (assert 
     (forall ((x Int) (y Int) (z Int)) 
          (=> (and (<= x 100) (mc (+ x 11) y) (mc y z)) 
              (mc x z))))
   (assert 
     (forall ((x Int) (y Int)) 
          (=> (and (<= x 101) (mc x y)) 
              (= y 91))))
   (check-sat)
   (get-model)

Horn Clause Engines

• PDR, SPACER - IC3 inspired engine [13, 23].
• Duality - Interpolation based [24].
  • Use Duality, PDR, or SPACER if your Horn clauses use arithmetic variables.
• Datalog - Bottom-up stratified Datalog engine for finite domains [14].
  • Use Datalog backened for Horn clauses over finite domains: bit-vectors and Booleans.
• BMC - Bounded model checking, Tabulation, Symbolic Execution…
  • Use BMC to unfold Horn clauses a la bounded model checking.

IC3

• are state variables.

• is a monome (a conjunction of literals).

• is a clause (a disjunction of literals).
  
  

• Convention: is a monome over variables , is a renaming of the same monome to variables .

IC3 recap

• - a transition system.
• - good states.
• - forward predicate transformer.
  • Given reachable states , produce “states can be reached by including another step”.
  • From Transition System:
  • From Horn Clauses: , where

IC3 recap (2)

• properties of states reachable within steps.
• are sets of clauses.
• Initially .
• a queue of counter-example trace properties. Initially .
• a level indication. Initially .

Expanding Traces

repeat until ∞

• Candidate If for some , , then add to .
  

• Unfold If , then set .
  

Termination

repeat until ∞

• Unreachable For , if , return Unreachable.

• Reachable If , return Reachable.
  

Search

repeat until ∞

• Decide Add to if
  
  • ,
    
  • is consistent, and