# Playing with Quantifier Satisfaction

 Nikolaj Bjørner and Mikoláš Janota Microsoft Research nbjorner@microsoft.com, mikolas.janota@gmail.com

## Quantified Formulae

• a game between universal and existential player
• E.g. , winning strategy

### Solving QBF (QESTO)

• : starts. is false.
• : strikes back. is true.
• : has to backtrack. is already unsat.
• : learns .
• : is false.
• : counters - is true.
• : has yet again to consider what went wrong by determining the core , which is empty. The universal player has to give up and the existential player established that the formula is true.

### Model-based Projections

• , , and .
• The size of is no larger than the size of .
• There is a sequence of models of , such that .
• Let be an infinite sequence of models of literals , then there is a finite set of equivalent projections .

### Model-based Projection

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

### 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          

### Proof

Note: core for is implicant of .

### On Quantifier Elimination

• Extends to Quantifier Elimination.

• Enumerate literals that imply

• by tracking clauses asserted at level 2.

### On Strategies

• Our base strategy uses limited look-ahead.

• It is possible to formulate stronger strategies (based on models)

### Some Experiments

 Figure 1. LRA Figure 2. LIA

### Summary and Future Work

• Solving quantified theories.
• Using Model-based projections and cores.
• Symmetric view on and .
• More theories?