- 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.
- , , 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 .
def sign(M,a): if M(a) return a else return a
Model-based Projection for LRA
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
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
M = null
M = current model
j = j + 1
Note: core for is implicant of .
On Quantifier Elimination
Extends to Quantifier Elimination.
Enumerate literals that imply
by tracking clauses asserted at level 2.
Summary and Future Work
- Solving quantified theories.
- Using Model-based projections and cores.
- Symmetric view on and .
- More theories?
- More advances lookahead? (hints in afternoon talk)