Playing with Quantifier Satisfaction

Nikolaj Bjørner and Mikoláš Janota
Microsoft Research

Quantified Formulae

\[\begin{mdMathprearray}%mdk
\forall \mathid{x}_1\exists \mathid{x}_2\dots.\ \mathid{F}
\end{mdMathprearray}%mdk
\]
  • a game between universal and existential player
  • E.g. $\forall x\exists y.\ x\leq y$, winning strategy $y\triangleq x+1$

Solving QBF (QESTO)

\[\begin{mdMathprearray}%mdk
\mathid{G}\mdMathspace{2}=\mdMathspace{2}(\forall \mathid{u}_1\mdMathspace{1}\mathid{u}_2\exists \mathid{e}_1\mdMathspace{1}\mathid{e}_2.\,\mathid{F}),\mdMathspace{2}\mathid{F}=(\mathid{u}_1\mdMathspace{1}\land \mathid{u}_2\mdMathspace{1}\rightarrow  \mathid{e}_1)\mdMathspace{1}\land (\mathid{u}_1\mdMathspace{1}\land \neg \mathid{u}_2\mdMathspace{1}\rightarrow \mathid{e}_2)\mdMathspace{1}\land(\mathid{e}_1\mdMathspace{1}\land \mathid{e}_2\mdMathspace{1}\rightarrow \neg \mathid{u}_1)
\end{mdMathprearray}%mdk
\]
  • $\forall$: starts. $F \wedge u_1 \wedge u_2 \wedge \overline{e}_1 \wedge \overline{e}_2$ is false.
  • $\exists$: strikes back. $F \wedge u_1 \wedge u_2 \wedge e_1 \wedge \overline{e}_2$ is true.
  • $\forall$: has to backtrack. $F\land u_2 \land e_1 \land \overline{e}_2$ is already unsat.
  • $\forall$: learns $\neg u_2$.
  • $\forall$: $\overline{u}_2 \land F \land u_1 \land \overline{e}_1 \land \overline{e}_2$ is false.
  • $\exists$: counters - $\overline{u}_2 \land F \land u_1 \land e_1 \land e_2$ is true.
  • $\forall$: has yet again to consider what went wrong by determining the core $\overline{u}_2 \land \neg F \land \overline{e}_1 \land e_2$, which is empty. The universal player has to give up and the existential player established that the formula is true.

Model-based Projections $\Mbp(M, \vec{x}, F)$

  • $FV(\varphi) \cap \vec{x} = \emptyset$, $M \models \varphi$, and $\varphi \Rightarrow \exists \vec{x} F$.
  • The size of $\Mbp(M, x, F)$ is no larger than the size of $F$.
  • There is a sequence $M_1, \ldots, $ of models of $F$, such that $(\exists x \ . \ F)\quad \equiv\quad \bigvee_i \Mbp(M_i, x, F)$.
  • Let $M_1, M_2, \ldots, $ be an infinite sequence of models of literals $F$, then there is a finite set of equivalent projections $\Mbp(M_i, x, F)$.

Model-based Projection

\[\begin{mdMathprearray}%mdk
\Mbp(\mathid{M},\mdMathspace{1}\emptyset,\mdMathspace{1}\varphi)\mdMathspace{8}=\mdMathspace{2}\varphi \mdMathbr{}
\Mbp(\mathid{M},\mdMathspace{1}\vec{\mathid{x}},\mdMathspace{1}\varphi)\mdMathspace{9}=\mdMathspace{2}\Mbp\left(\mathid{M},\mdMathspace{1}\vec{\mathid{x}},\mdMathspace{1}\bigwedge \{\mdMathspace{1}\mathid{sign}(\mathid{M},\mdMathspace{1}\mathid{a})\mdMathspace{1}\;\mid\;\mdMathspace{1}\mathid{a}\mdMathspace{1}\mbox{ is an atom in }\mdMathspace{1}\varphi \}\right)\mdMathspace{1}\mdMathbr{}
\Mbp(\mathid{M},\mdMathspace{1}\mathid{x}\vec{\mathid{x}},\mdMathspace{1}\varphi)\mdMathspace{7}=\mdMathspace{2}\Mbp(\mathid{M},\mdMathspace{1}\mathid{x},\mdMathspace{1}\Mbp(\mathid{M},\mdMathspace{1}\vec{\mathid{x}},\mdMathspace{1}\varphi))\mdMathspace{1}\mdMathbr{}
\Mbp(\mathid{M},\mdMathspace{1}\mathid{x},\mdMathspace{1}\varphi \land \psi)\mdMathspace{2}=\mdMathspace{2}\Mbp(\mathid{M},\mdMathspace{1}\mathid{x},\mdMathspace{1}\varphi)\mdMathspace{1}\land \psi   \quad\quad    \mathid{if}\mdMathspace{1}\mathid{x}\mdMathspace{1}\not\in \mathid{FV}(\psi)\mdMathspace{1}
\end{mdMathprearray}%mdk
\]
   def sign(M,a): if M(a) return a else return $\neg$a

Model-based Projection for LRA

\[\begin{mdMathprearray}%mdk
\Mbp(\mathid{M},\mdMathspace{1}\mathid{x},\mdMathspace{1}\mathid{x}\mdMathspace{1}\simeq \mathid{t}\mdMathspace{1}\land \mathid{L})\mdMathspace{2}=\mdMathspace{2}\mathid{L}[\mathid{t}/\mathid{x}]\mdMathspace{1}\mdMathbr{}
\Mbp(\mathid{M},\mdMathspace{1}\mathid{x},\mdMathspace{1}\mathid{x}\mdMathspace{1}\not\simeq \mathid{t}\mdMathspace{1}\land \mathid{L})\mdMathspace{1}=\mdMathspace{2}\Mbp(\mathid{M},\mdMathspace{1}\mathid{x},\mdMathspace{1}\mathid{x}\mdMathspace{1}\geq \mathid{t}\mdMathspace{1}+\mdMathspace{1}\epsilon \land \mathid{L})\mdMathspace{1}\quad \mbox{if}\quad \mathid{M}(\mathid{x})\mdMathspace{1}>\mdMathspace{1}\mathid{M}(\mathid{t})\mdMathspace{1}\mdMathbr{}
\Mbp(\mathid{M},\mdMathspace{1}\mathid{x},\mdMathspace{1}\mathid{x}\mdMathspace{1}\not\simeq \mathid{t}\mdMathspace{1}\land \mathid{L})\mdMathspace{1}=\mdMathspace{2}\Mbp(\mathid{M},\mdMathspace{1}\mathid{x},\mdMathspace{1}\mathid{x}\mdMathspace{1}+\mdMathspace{1}\epsilon \leq \mathid{t}\mdMathspace{1}\land \mathid{L})\mdMathspace{1}\quad \mbox{if}\quad \mathid{M}(\mathid{x})\mdMathspace{1}<\mdMathspace{1}\mathid{M}(\mathid{t})\mdMathspace{1}\mdMathbr{}
\Mbp(\mathid{M},\mdMathspace{1}\mathid{x},\mdMathspace{1}\bigwedge_\mathid{i}\mdMathspace{1}\mathid{t}_\mathid{i}\mdMathspace{1}\leq \mathid{x}\mdMathspace{1}\land \bigwedge_\mathid{j}\mdMathspace{1}\mathid{x}\mdMathspace{1}\leq \mathid{s}_\mathid{j})\mdMathspace{1}=\mdMathspace{2}\bigwedge_\mathid{i}\mdMathspace{1}\mathid{t}_\mathid{i}\mdMathspace{1}\leq \mathid{t}_0\mdMathspace{1}\land \bigwedge_\mathid{j}\mdMathspace{1}\mathid{t}_0\mdMathspace{1}\leq \mathid{s}_\mathid{j}\mdMathspace{1}\\\mdMathbr{}
\mdMathindent{13}\mathid{where}\mdMathspace{1}\mathid{M}(\mathid{t}_0)\mdMathspace{1}\geq \mathid{M}(\mathid{t}_\mathid{i})\mdMathspace{1}\forall \mathid{i}
\end{mdMathprearray}%mdk
\]

Initialization

\[\begin{mdMathprearray}%mdk
\mdMathindent{4}\exists \mathid{x}_{1},\mdMathspace{1}\forall \mathid{x}_{2},\mdMathspace{1}\exists \mathid{x}_{3},\mdMathspace{1}\forall \mathid{x}_{4},\mdMathspace{1}….,\mdMathspace{1}\mathid{Q}\mdMathspace{1}\mathid{x}_{\mathid{n}}\mdMathspace{1}\mathid{F}[\mathid{x}_{1},\mdMathspace{1}\mathid{x}_{2},\mdMathspace{1}\ldots]\mdMathbr{}
\mathid{Initialize}:\mdMathbr{}
\mdMathindent{4}\mathid{F}_\mathid{j}\mdMathspace{13}\leftarrow \mathid{F}\mdMathspace{11}\mathid{if}\mdMathspace{1}\mathid{j}\mdMathspace{1}\mathid{is}\mdMathspace{1}\mathid{odd}\mdMathbr{}
\mdMathindent{4}\mathid{F}_\mathid{j}\mdMathspace{13}\leftarrow \neg \mathid{F}\mdMathspace{8}\mathid{if}\mdMathspace{1}\mathid{j}\mdMathspace{1}\mathid{is}\mdMathspace{1}\mathid{even}
\end{mdMathprearray}%mdk
\]
   def level(j,a): return max level of bound variable in atom a of parity j     
\[\begin{mdMathprearray}%mdk
\mdMathindent{3}\mathid{level}(1,\mdMathspace{1}\mathid{z}\mdMathspace{1}\geq 0)\mdMathspace{1}=\mdMathspace{1}\mathid{level}(3,\mdMathspace{1}\mathid{z}\mdMathspace{1}\geq 0)\mdMathspace{1}=\mdMathspace{1}3\mdMathbr{}
\mdMathindent{3}\mathid{level}(2,\mdMathspace{1}\mathid{z}\mdMathspace{1}\geq 0)\mdMathspace{1}=\mdMathspace{1}0\mdMathbr{}
\mdMathindent{3}\mathid{in}\mdMathspace{1}\exists \mathid{x}\mdMathspace{1}\forall \mathid{y}\mdMathspace{1}\exists \mathid{z}\mdMathspace{1}\mathid{z}\mdMathspace{1}\geq 0\mdMathspace{1}\land ((\mathid{x}\mdMathspace{1}\geq 0\mdMathspace{1}\land \mathid{y}\mdMathspace{1}\geq 0)\mdMathspace{1}\lor \mathid{y}\mdMathspace{1}+\mdMathspace{1}\mathid{z}\mdMathspace{1}\leq 1)
\end{mdMathprearray}%mdk
\]

Property Directed QSAT Algorithm

  def strategy(M,j): return $\bigwedge_{M \neq null, a \in Atoms, level(j, a) < j} sign(M,a) $
def tailv(j): return $x_{j-1},x_j,x_{j+1},\ldots$

j = 1
M = null
while True:
if $F_{j}\ \ \land$ strategy(M, j) is unsat:
if j == 1:
return F is unsat
if j == 2:
return F is sat
C = Core($F_j$, strategy(M, j))
J = Mbp(tailv(j), C)
j = index of max variable in J $\cup\ \{ 1, 2 \}$ of same parity as j
$F_j$ = $F_j \land \neg $J
M = null
else:
M = current model
j = j + 1

Proof

\[\begin{mdMathprearray}%mdk
\mdMathindent{12}\mathid{F}_\mathid{j}\mdMathspace{1}\land \mathid{strategy}(\mathid{M},\mdMathspace{1}\mathid{j})\mdMathspace{3}\mathid{is}\mdMathspace{1}\mathid{unsat}\mdMathbr{}
\mdMathbr{}
\mdMathindent{12}\mathid{F}_\mathid{j}\mdMathspace{1}\rightarrow \neg \mathid{C}\mdMathspace{13}\mathid{where}\mdMathspace{5}\mathid{C}\mdMathspace{1}=\mdMathspace{1}\mathid{Core}(\mathid{F}_\mathid{j},\mdMathspace{1}\mathid{strategy}(\mathid{M},\mdMathspace{1}\mathid{j}))\mdMathspace{1}\mdMathbr{}
\mdMathbr{}
\mdMathindent{12}\mathid{J}\mdMathspace{1}\rightarrow \exists \mathid{tailv}(\mathid{j})\mdMathspace{1}\mathid{C}\mdMathspace{2}\mathid{where}\mdMathspace{5}\mathid{J}\mdMathspace{1}=\mdMathspace{1}\Mbp(\mathid{tailv}(\mathid{j}),\mdMathspace{1}\mathid{C})\mdMathbr{}
\mdMathbr{}
\mdMathindent{12}\forall \mathid{tailv}(\mathid{j})\mdMathspace{1}\neg \mathid{C}\mdMathspace{1}\rightarrow \neg \mathid{J}\mdMathbr{}
\mdMathbr{}
\mdMathindent{12}\forall \vec{\mathid{x}}_{\mathid{j}-1}\exists \vec{\mathid{x}}_\mathid{j}\mdMathspace{1}\forall \vec{\mathid{x}}_{\mathid{j}+1}\mdMathspace{1}\ldots \mathid{F}_\mathid{j}\mdMathspace{1}\rightarrow \forall \vec{\mathid{x}}_{\mathid{j}-1}\exists \vec{\mathid{x}}_\mathid{j}\mdMathspace{1}\forall \vec{\mathid{x}}_{\mathid{j}+1}\mdMathspace{1}\ldots \neg \mathid{C}\mdMathspace{1}\rightarrow \neg \mathid{J}\mdMathbr{}
\mdMathindent{13}\mdMathbr{}
\mdMathindent{12}\mathid{because}\mdMathspace{1}\vec{\mathid{x}}_\mathid{j},\mdMathspace{1}\vec{\mathid{x}}_{\mathid{j}+2},\mdMathspace{1}\vec{\mathid{x}}_{\mathid{j}+4},\ldots \not\in \mathid{FV}(\mathid{C})
\end{mdMathprearray}%mdk
\]

Note: core for $F_j$ is implicant of $\neg F_j$.

On Quantifier Elimination

  • Extends to Quantifier Elimination.

  • Enumerate literals that imply $\neg F[x]$

  • 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

lra


Figure 1. LRA

lia


Figure 2. LIA

Summary and Future Work

  • Solving quantified theories.
  • Using Model-based projections and cores.
  • Symmetric view on $\exists$ and $\forall$.
  • More theories?
  • More advances lookahead? (hints in afternoon talk)