Playing with Quantifier Satisfaction

Nikolaj Bjørner and Mikoláš Janota

Microsoft Research

nbjorner@microsoft.com, mikolas.janota@gmail.com

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

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)