# 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

### Model-based Projection for LRA ### 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?