Nikolaj Bjørner and Mikoláš Janota
Microsoft Research
nbjorner@microsoft.com, mikolas.janota@gmail.com |
def sign(M,a): if M(a) return a else return a
def level(j,a): return max level of bound variable in atom a of parity j
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
Note: core for is implicant of .
Extends to Quantifier Elimination.
Enumerate literals that imply
by tracking clauses asserted at level 2.
Our base strategy uses limited look-ahead.
It is possible to formulate stronger strategies (based on models)