11institutetext:  TU Wien, Vienna, Austria
11email<EMAIL_ADDRESS>
# Certified DQBF Solving by Definition Extraction

Franz-Xaver Reichl  Friedrich Slivovsky  Stefan Szeider

###### Abstract

We propose a new decision procedure for dependency quantified Boolean formulas
(DQBFs) that uses interpolation-based definition extraction to compute Skolem
functions in a counter-example guided inductive synthesis (CEGIS) loop. In
each iteration, a family of candidate Skolem functions is tested for
correctness using a SAT solver, which either determines that a model has been
found, or returns an assignment of the universal variables as a
counterexample. Fixing a counterexample generally involves changing candidates
of multiple existential variables with incomparable dependency sets. Our
procedure introduces auxiliary variables—which we call _arbiter variables_
—that each represent the value of an existential variable for a particular
assignment of its dependency set. Possible repairs are expressed as clauses on
these variables, and a SAT solver is invoked to find an assignment that deals
with all previously seen counterexamples. Arbiter variables define the values
of Skolem functions for assignments where they were previously undefined, and
may lead to the detection of further Skolem functions by definition
extraction.

A key feature of the proposed procedure is that it is certifying by design:
for true DQBF, models can be returned at minimal overhead. Towards
certification of false formulas, we prove that clauses can be derived in an
expansion-based proof system for DQBF.

In an experimental evaluation on standard benchmark sets, a prototype
implementation was able to match (and in some cases, surpass) the performance
of state-of-the-art-solvers. Moreover, models could be extracted and validated
for all true instances that were solved.

##  1 Introduction

Sustained progress in propositional satisfiability (SAT) solving [23] has
resulted in a growing number of applications in the area of electronic design
automation [49], such as model checking [7], synthesis [43], and symbolic
execution [5]. Efficient SAT solvers were essential for recent progress in
constrained sampling and counting [31], two problems with many applications in
artificial intelligence. In these cases, SAT solvers are used to deal with
problems from complexity classes beyond NP and propositional encodings that
grow super-polynomially in the size of the original instances. As a
consequence, these problems are not directly encoded in propositional logic
but have to be reduced to a sequence of SAT instances.

The success of SAT solving on the one hand, and the inability of propositional
logic to succinctly encode problems of interest on the other hand, have
prompted the development of decision procedures for more succinct
generalizations of propositional logic such as Quantified Boolean Formulas
(QBFs). Evaluating QBFs is PSPACE-complete [45] and thus believed to be much
harder than SAT, but in practice the benefits of a smaller encoding may
outweigh the disadvantage of slower decision procedures [13]. A QBF is true if
it has a _model_ , which is a family of Boolean functions (often called
_Skolem functions_) that satisfy the matrix of the input formula for each
assignment of universal variables. The arguments of each Skolem function are
implicitly determined by the nesting of existential and universal quantifiers.
Dependency QBF (DQBF) explicitly state a _dependency set_ for each existential
variable, which is a subset of universal variables allowed as arguments of the
corresponding Skolem function [3, 4]. As such, they can succinctly encode the
existence of Boolean functions subject to a set of constraints [34], and
problems like equivalence checking of partial circuit designs [19] and bounded
synthesis [13] can be naturally expressed in this way.

Several decision procedures for DQBF have been developed in recent years (see
Section 5). Conceptually, these solvers either reduce to SAT or QBF by
instantiating [16] or eliminating universal variables [20, 50, 18, 39], or
lift Conflict-Driven Clause Learning (CDCL) to non-linear quantifier prefixes
by imposing additional constraints [15, 47].111An approach that does not fit
this simplified classification is the First-Order solver iProver [29]. We
believe these methods should be complemented with algorithms that directly
reason at the level of Skolem functions [35]. A strong argument in favor of
such an approach is the fact that DQBF instances often have a large fraction
of unique Skolem functions that can be obtained by definition extraction, but
the current solving paradigms have no direct way of exploiting this [40].

In this paper, we develop new decision procedures for DQBF designed around
computing Skolem functions by definition extraction. We first describe a
simple algorithm that proceeds in two phases. In the first phase, it
introduces clauses to make sure each existential variable is defined in terms
of its dependency set and auxiliary _arbiter variables_. In the second phase,
it searches for an assignment of the arbiter variables under which the
definitions are a model. Runs of this algorithm can degenerate into an
exhaustive instantiation of dependency sets for easy cases, so we propose an
improved version in the Counter-Example Guided Inductive Synthesis (CEGIS)
paradigm [43, 42, 28].

We implemented the CEGIS algorithm in a system named Pedant. In an
experimental evaluation, Pedant performs very well compared to a selection of
state-of-the-art solvers—notably, it achieves good performance without the aid
of the powerful preprocessor HQSPre [51]. One of the benefits of its function-
centric design is that Pedant internally computes a family of Skolem
functions, and can output models of true instances at a negligible overhead.
Using a simple workflow, we are able to validate models for all true instances
solved by Pedant. Towards validation of false instances, we prove that clauses
introduced by Pedant can be derived in the $\forall$Exp+Res proof system [27,
6].

The remainder of the paper is structured as follows. After covering basic
concepts in Section 2, we present the new decision algorithms for DQBF and
prove their correctness in Section 3. We describe the implementation and
experimental results in Section 4. We discuss related work in Section 5,
before concluding with an outlook on future work in Section 6.

##  2 Preliminaries

##### Propositional Logic

A _literal_ is either a variable or the negation of a variable. A _clause_ is
the disjunction of literals. A _term_ is a conjunction of literals. A formula
is in _Conjunctive Normal Form_ (CNF) if it is a conjunction of clauses.
Whenever convenient, we identify a CNF with a set of clauses and clauses,
respectively terms, with sets of literals. We denote the set of variables
occurring in a formula $\varphi$ by $\mathit{var}(\varphi)$. We denote the
truth value _true_ by true and _false_ by false. An _assignment_ of a set $V$
of variables is a function mapping $V$ to
$\\{\textsc{true},\textsc{false}\\}$. We denote the set of all assignments for
$V$ by $[V]$. Moreover, we associate an assignment $\sigma$ with the term
$\\{x\mid x\in\mathbf{dom}(\sigma),\sigma(x)=\textsc{true}\\}\cup\\{\neg x\mid
x\in\mathbf{dom}(\sigma),\sigma(x)=\textsc{false}\\}$. Whenever convenient, we
treat assignments as terms. Let $\sigma\in[V]$ and let $W\subseteq V$, then we
denote the _restriction of $\sigma$ to $W$_ by
${\left.\kern-1.2pt\sigma\right|_{W}}$. For a formula $\varphi$ and an
assignment $\sigma$ we denote the _evaluation of $\varphi$ by $\sigma$_ with
$\varphi[\sigma]$. A formula $\varphi$ is _satisfied_ by an assignment
$\sigma$ if $\varphi[\sigma]=\textsc{true}$ and it is _falsified_ by $\sigma$
otherwise. A formula $\varphi$ is _satisfiable_ if there is an assignment
$\sigma$ that satisfies $\varphi$ and it is _unsatisfiable_ otherwise. Let
$\varphi$ and $\psi$ be two formulae, $\varphi$ _entails_ $\psi$, denoted by
$\varphi\vDash\psi$, if every assignment satisfying $\varphi$ also satisfies
$\psi$. A _definition_ for a variable $x$ by a set of variables $X$ in a
formula $\varphi$ is a formula $\psi$ with $\mathit{var}(\psi)\subseteq X$
such that for every satisfying assignment $\sigma$ of $\varphi$ the equality
$\sigma(x)=\psi[\sigma]$ holds [40].

##### Dependency Quantified Boolean formulas

We only consider _Dependency Quantified Boolean formulas_ (DQBF) in _Prenex
Conjunctive Normal Form_ (PCNF). A DQBF in PCNF is denoted by
$\Phi=\mathcal{Q}.\varphi$, where  (a) the _quantifier prefix_ $\mathcal{Q}$
is given by $\mathcal{Q}=\forall u_{1}\ldots\forall u_{n}\exists
e_{1}(D_{1})\ldots\exists e_{m}(D_{m})$. Here $u_{1},\ldots,u_{n}$ and
$e_{1},\ldots,e_{m}$ shall be pairwise different variables. We denote the set
$\\{u_{1},\ldots,u_{n}\\}$ by $U_{\Phi}$ and the set
$\\{e_{1},\ldots,e_{m}\\}$ by $E_{\Phi}$. Additionally, $D_{1},\ldots,D_{m}$
shall be subsets of $U_{\Phi}$.  (b) the _matrix_ $\varphi$ shall be a CNF
with $\mathit{var}(\varphi)\subseteq U_{\Phi}\cup E_{\Phi}$.  For $1\leq i\leq
m$ we call the set $D_{i}$ the _dependencies_ of $e_{i}$. We refer to the
variables in $U_{\Phi}$ as _universal variables_ and to the variables in
$E_{\Phi}$ as _existential variables_. For an existential variable $e$ we
denote its dependencies by $D_{\Phi}(e)$. If the underlying DQBF is clear from
the context we omit the subscript.

Let $\Phi$ be a DQBF and $F$ be a set of functions
$\\{f_{e_{1}},\ldots,f_{e_{m}}\\}$ such that for $1\leq i\leq m$,
$f_{e_{i}}:[D_{i}]\rightarrow\\{\textsc{true},\textsc{false}\\}$. For an
assignment $\sigma$ to the universal variables we denote the existential
assignment
$\\{f_{e_{1}}({\left.\kern-1.2pt\sigma\right|_{D_{1}}}),\ldots,f_{e_{m}}({\left.\kern-1.2pt\sigma\right|_{D_{m}}})\\}$
by $F(\sigma)$. $F$ is a _model_ (or a _winning $\exists$-strategy_) for
$\Phi$ if for each assignment $\sigma$ to the universal variables, the
assignment $\sigma\cup F(\sigma)$ satisfies the matrix $\varphi$. A DQBF is
true if it has a model and false otherwise.

#####  $\forall$Exp+Res

The _DQBF- $\forall$Exp+Res_ [6] calculus is a proof system for DQBF, which is
based on the _$\forall$ Exp+Res_ calculus for QBF. It instantiates the matrix
of a DQBF with a universal assignment and uses propositional resolution on the
instantiated clauses. This proof system is sound and refutationally complete
[6]. Since we are interested in DQBF, we refer to DQBF-$\forall$Exp+Res simply
as $\forall$Exp+Res. The rules for the system are given in Fig. 1.

(axiom)
$\\{\ell^{{\left.\kern-1.2pt\sigma\right|_{D(\mathit{var}(\ell))}}}\mid\ell\in
C,\mathit{var}(\ell)\in E\\}$ Where $C$ is a clause in the matrix of the DQBF
and $\sigma$ is an assignment to the universal variables that falsifies each
universal literal in $C$. Note that variables with a different annotation
denote different variables. The second rule is the propositional resolution
rule. $C_{1}\cup\\{x^{\tau}\\}$ $C_{2}\cup\\{\neg x^{\tau}\\}$ (resolution)
$C_{1}\cup C_{2}$ Where $x$ is an existential variable, $\tau$ an assignment
for the universal variables in $D(e)$ and where $C_{1}$ and $C_{2}$ are
clauses. Figure 1: The rules of DQBF-$\forall$Exp+Res

##  3 Solving DQBF by Definition Extraction

In this section, we describe two decision procedures for DQBF that leverage
definition extraction. We start with an algorithm (Algorithm 1) that is fairly
simple but introduces some important concepts. Because this algorithm leads to
the equivalent of exhaustive expansion of universal variables on trivial
examples, we then introduce a more sophisticated algorithm based on CEGIS
(Algorithm 2). We also sketch correctness proofs for both algorithms.

Throughout this section, we consider a fixed DQBF
$\Phi\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\mathcal{Q}.\;\varphi$
with quantifier prefix
$\mathcal{Q}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\forall
u_{1}\ldots\forall u_{n}\allowbreak\exists e_{1}(D_{1})\ldots\exists
e_{m}(D_{m})$.

###  3.1 A Two-Phase Algorithm

The algorithm proceeds in two phases. In the first phase
(GenerateDefinitions), it finds definitions $\psi_{\mathit{Def}}$ for all
existential variables. It maintains a set $A$ of auxiliary _arbiter variables_
whose semantics are encoded in a set $\varphi_{A}$ of _arbiter clauses_ , both
of which are empty initially. If a variable $e_{i}$ is defined in terms of its
dependency set, the definition is computed using a SAT solver (line 16)
capable of generating interpolants [40]. Otherwise, the SAT solver returns an
assignment $\xi$ of the dependency set $D_{i}$ and the arbiter variables $A$
for which the variable is not defined. In particular, $e_{i}$ is not defined
under the restriction $\sigma=\xi|_{D_{i}}$ to its dependency set. The
algorithm then introduces an arbiter variable $e_{i}^{\sigma}$ that determines
the value of the Skolem function for $e_{i}$ under $\sigma$. In subsequent
iterations, we include these arbiter variables in the set of variables that
can be used in a definition of $e_{i}$. The newly introduced clauses ensure
that $e_{i}$ and $e_{i}^{\sigma}$ take the same value under the assignment
$\sigma$ (line 14), so that $e_{i}$ is defined by $e_{i}^{\sigma}$ and
$D_{i}$. Since the number of assignments $\sigma$ of the dependency set is
bounded, we will eventually find a definition of $e_{i}$ in terms of its
dependency set $D_{i}$ and the arbiter variables $A$.

In the second phase (FindArbiterAssignment), a SAT solver (line 23) is used to
find an assignment of the arbiter variables under which the definitions
obtained in the first phase are a model. Starting with an initial assignment
$\tau$, we use a SAT solver to check whether the formula
$\psi_{\mathit{Def}}\land\neg\varphi$ consisting of the definitions from the
first phase and the negated matrix of the input DQBF is unsatisfiable under
$\tau$ (line 25). If that is the case, Algorithm 1 returns true. Otherwise,
the SAT solver returns an assignment $\sigma$ as a counterexample. Since the
existential variables are defined in $\varphi\land\varphi_{A}$ by the
universal and arbiter variables, the formula $\varphi\land\varphi_{A}$ must be
unsatisfiable under the assignment $\tau\land\sigma|_{U}$ consisting of the
arbiter assignment and counterexample restricted to universal variables. A
_core_ $\rho$ of failed assumptions $\tau\land\sigma_{U}$ such that
$\rho\models\neg(\varphi\land\varphi_{A})$ is extracted using another SAT
call. The assignment $\rho|_{A}$ represents a concise reason for the failure
of the arbiter assignment $\tau$, and its negation $\neg\rho|_{A}$ is added as
a new clause to the SAT solver used to generate arbiter assignments, which is
subsequently invoked to find a new arbiter assignment.

This process continues until a model is found or the SAT solver cannot find a
new arbiter assignment, in which case the algorithm returns false.

Algorithm 1 Solving DQBF by Definition Extraction

1:procedure SolveByDefinitionExtraction($\Phi$)

2:
$(\varphi_{A},A,\psi_{\mathit{Def}})\leftarrow\textsc{GenerateDefinitions}(\Phi)$

3: return
$\textsc{FindArbiterAssignment}(\Phi,\varphi_{A},A,\psi_{\mathit{Def}})$

4:

5:procedure GenerateDefinitions($\Phi$)

6: $\triangleright$ $\Phi=\forall u_{1}\ldots\forall u_{n}\exists
e_{1}(D_{1})\ldots\exists e_{m}(D_{m}).\varphi$

7:
$A\leftarrow\emptyset,\;\psi_{\mathit{Def}}\leftarrow\emptyset,\;\varphi_{A}\leftarrow\emptyset$

8: $\triangleright$ $A$: arbiter variables, $\psi_{\mathit{Def}}$:
definitions, $\varphi_{A}$: arbiter clauses

9: for $i=1,\dots,m$ do

10: $\mathit{isDefined},\xi\leftarrow\textsc{isDefined}(e_{i},A\cup
D_{i},\varphi\wedge\varphi_{A})$

11: while not $\mathit{isDefined}$ do

12: $\sigma\leftarrow{\left.\kern-1.2pt\xi\right|_{D_{i}}}$ $\triangleright$
$e_{i}$ is not defined under $\xi\in[D_{i}\cup A]$

13: $A\leftarrow A\cup\\{e^{\sigma}_{i}\\}$

14:
$\varphi_{A}\leftarrow\varphi_{A}\wedge(e^{\sigma}_{i}\vee\neg\sigma\vee\neg
e_{i})\wedge(\neg e^{\sigma}_{i}\vee\neg\sigma\vee e_{i})$

15: $\mathit{isDefined},\xi\leftarrow\textsc{isDefined}(e_{i},A\cup
D_{i},\varphi\wedge\varphi_{A})$

16: $\psi_{\mathit{Def}}^{i}\leftarrow\textsc{getDefinition}(e_{i},A\cup
D_{i},\varphi\wedge\varphi_{A})$

17:
$\psi_{\mathit{Def}}\leftarrow\psi_{\mathit{Def}}\wedge(e_{i}\leftrightarrow\psi_{\mathit{Def}}^{i})$

18: return $(\varphi_{A},A,\psi_{\mathit{Def}})$

19:

20:procedure FindArbiterAssignment($\Phi,\varphi_{A},A,\psi_{\mathit{Def}}$)

21: $\tau\leftarrow\bigwedge_{a\in A}a$ $\triangleright$ initial assignment to
the arbiter variables

22:
$\mathit{validitySolver}\leftarrow\textsc{SatSolver}(\mathit{\psi_{\mathit{Def}}}\wedge\neg\varphi)$

23: $\mathit{arbiterSolver}\leftarrow\textsc{SatSolver}(\emptyset)$

24: loop

25: if $\mathit{validitySolver}.\textsc{solve}(\tau)$ then

26: $\sigma\leftarrow\mathit{validitySolver}.\textsc{getModel}($)

27:
$\rho\leftarrow\textsc{getCore}(\varphi\wedge\varphi_{A},\tau\wedge{\left.\kern-1.2pt\sigma\right|_{U}})$

28:
$\mathit{arbiterSolver}.\textsc{addClause}(\neg{\left.\kern-1.2pt\rho\right|_{A}})$

29: if $\mathit{arbiterSolver}.\textsc{solve}()$ then

30: $\tau\leftarrow\mathit{arbiterSolver}.\textsc{getModel}($)

31: else

32: return false

33: else

34: return true

We now argue that Algorithm 1 is a decision procedure for DQBF. In the
following, $A$ shall denote a set of arbiter variables and $\varphi_{A}$ shall
denote the associated set of arbiter clauses. We will first give two auxiliary
properties of definitions, which we will use in subsequent proofs.

###### Lemma 1

Let $\varphi$ and $\xi$ be two propositional formulas, let
$e\in\mathit{var}(\varphi)$ and $S\subseteq\mathit{var}(\varphi)$. Moreover,
let $\psi_{\mathit{Def}}$ be a definition for $e$ by $S$ in $\varphi$. Then
$\psi_{\mathit{Def}}$ is also a definition for $e$ by $S$ in
$\varphi\wedge\xi$.

###### Proof

Obviously any satisfying assignment $\sigma$ of $\varphi\wedge\xi$ also
satisfies $\varphi$. By the premise of the lemma we know that for every
satisfying assignment $\sigma$ of $\varphi$ we have
$\sigma(e)=\psi_{\mathit{Def}}[\sigma]$. By combining the above two properties
we get that $\sigma(e)=\psi_{\mathit{Def}}[\sigma]$ holds for every satisfying
assignment for $\varphi\wedge\xi$. This proves the lemma.

###### Remark 1

The above Lemma implies that if we once find a definition in Algorithm 1 then
we do not destroy it by adding additional clauses.

###### Lemma 2

Let $\psi$ be a formula and let $S\subseteq\mathit{var}(\psi)$ such that each
$s\in S$ has a definition $\psi_{s}$ by a set
$D_{s}\subseteq\mathit{var}(\psi)$ in $\psi$. Then $\psi$ and
$\psi\wedge\bigwedge_{v\in S}(v\leftrightarrow\psi_{s})$ are equivalent.

###### Proof

First assume that $\psi$ is satisfied by an assignment $\sigma$. By the nature
of definition we have $\sigma(v)=\psi_{v}[\sigma]$ for each $v\in S$. Thus,
$\sigma$ satisfies $\psi\wedge\bigwedge_{v\in S}(v\leftrightarrow\psi_{s})$.
The other direction of the equivalence is obvious.

A DQBF has a model if, and only if, there is a propositional formula for each
existential variable that defines its Skolem functions using only variables
from the dependency set. This can be slightly generalized by allowing the
definition to contain existential variables whose dependency sets are a
subset.

###### Lemma 3

Let $\Phi$ be a DQBF and $<_{E}$ a linear ordering of its existential
variables. Then $\Phi$ is true if, and only if, for each $e\in E$ there is a
formula $\psi_{e}$ with $\mathit{var}(\psi_{e})\subseteq D(e)\cup\\{x\in E\mid
D(x)\subseteq D(e),x<_{E}e\\}$ such that $\neg\varphi\wedge\bigwedge_{e\in
E}(e\leftrightarrow\psi_{e})$ is unsatisfiable.

###### Proof

First we assume that $\Phi$ is true. This means that there is a model
$F=\\{f_{1},\ldots f_{m}\\}$. We can encode these functions by formulas
$\psi_{e}$. Obviously we have for each $e\in E$ that
$\mathit{var}(\psi_{e})\subseteq D(e)$—as the model function for $e$ may only
depend on $D(e)$. Now assume that $\neg\varphi\wedge\bigwedge_{e\in
E}(e\leftrightarrow\psi_{e})$ is satisfiable, i.e., there is an assignment
$\sigma$ that satisfies the formula. But this implies that there is an
assignment to the universal variables such that the matrix is falsified under
the model. As this contradicts our initial assumption, we know that the
formula is unsatisfiable.

Next we assume the other side of the equivalence and show how we can construct
a model for $\Phi$. For this purpose we distinguish between two cases. First
let $e$ be an existential variable such that $\mathit{var}(\psi_{e})\subseteq
D(e)$ and let $\sigma$ be an assignment to $D(e)$. Then we define
$f_{e}(\sigma)\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\psi_{e}[\sigma]$.
Now let $e$ be the smallest variable (with respect to $<_{E}$) in $E$ such
that $\mathit{var}(\psi_{e})\nsubseteq D(e)$. By using the assumption it
follows that for each variable $x\in\mathit{var}(\psi_{e})\setminus D(e)$ we
have $x<_{E}e$. Because of the minimality of $e$, this means that for each $x$
in $\mathit{var}(\psi_{e})\setminus D(e)$ we have already defined a function
$f_{x}$. Now we define for $\sigma\in[D(e)]$ the assignment
$\rho(\sigma)\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\\{(x,f_{x}({\left.\kern-1.2pt\sigma\right|_{D(x)}}))\mid
x\in\mathit{var}(\psi_{e})\setminus D(e)\\}.$ Finally, we define
$f_{e}(\sigma)\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\psi_{e}[\rho(\sigma)]$—the
construction guarantees that $\mathit{var}(\psi_{e}[\rho(\sigma)])\subseteq
D(e)$.

For the remaining variables we proceed inductively. We denote the resulting
set of functions by $F$. It remains to show that $F$ is actually a model. We
assume the opposite, i.e., there is a universal assignment $\sigma$ such that
$\varphi$ is falsified by $\sigma\cup F(\sigma)$. It can be proven that
$\sigma\cup F(\sigma)$ satisfies $\bigwedge_{e\in
E}(e\leftrightarrow\psi_{e})$. As $\sigma\cup F(\sigma)$ falsifies the matrix
$\varphi$ we get a contradiction to our initial assumption.

###### Theorem 3.1

If Algorithm 1 returns true for the DQBF $\Phi$ then $\Phi$ is true.

###### Proof

Let
$\Phi^{\prime}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\mathcal{Q}\exists
A(\emptyset).\varphi$, and let $<_{E}$ be any ordering of existential
variables in $\Phi^{\prime}$ in which the variables in $A$ come before the
remaining variables. If Algorithm 1 returns true, we know that there is an
arbiter assignment $\tau$ such that
$\neg\varphi\wedge\psi_{\mathit{Def}}\wedge\tau$ is unsatisfiable. For each
arbiter variable $e^{\sigma}$, we obtain a definition $\psi_{e}^{\sigma}$ as
$\psi_{e}^{\sigma}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\tau(e^{\sigma})$.
We can now replace the arbiter assignment $\tau$ with these definitions and
apply Lemma 3 to conclude that $\Phi^{\prime}$ is true. But if $\Phi^{\prime}$
is true, then necessarily also $\Phi$ is true.

To show that the algorithm returns false only if the input DQBF is false, one
can prove that clauses on arbiter variables introduced by
FindArbiterAssignment can be derived (as clauses on annotated literals) in
$\forall$Exp+Res.

###### Definition 1

Let $\tau$ be a (partial) assignment to the arbiter variables and let $\rho$
be an assignment to the universal variables. We define the term
$\tau^{\rho}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\\{\ell^{\sigma}\in\tau\mid\rho\vDash\sigma\\}$

###### Definition 2

Let $\sigma$ be an assignment to the universal variables. We denote the
formula that is the result of instantiating $\varphi$ by $\sigma$ in the sense
of the $\forall$Exp+Res calculus by $\varphi^{\rho}$. This means:

$\varphi^{\sigma}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\\{\\{x^{{\left.\kern-1.2pt\sigma\right|_{D(\mathit{var}(x))}}}\mid
x\in C,\mathit{var}(x)\in E\\}\mid C\in\varphi,\forall\ell\in
C:\mathit{var}(\ell)\in U\Rightarrow\sigma\nvDash\ell\\}$

###### Remark 2

Subsequently, we say that an arbiter clause
$C=\ell^{\sigma}\vee\neg\sigma\vee\neg\ell$ is active with respect to an
assignment $\rho$ if $\rho$ falsifies $\ell^{\sigma}$ and $\rho$ satisfies
$\sigma$.

###### Lemma 4

Let $\tau$ be a (partial) arbiter assignment and $\rho$ a universal
assignment. Then $\varphi\wedge\varphi_{A}\wedge\tau\wedge\rho$ and
$\varphi^{\rho}\wedge\tau^{\rho}$ are equisatisfiable.

###### Proof

First we assume that $\varphi\wedge\varphi_{A}\wedge\tau\wedge\rho$ is
satisfied by an assignment $\lambda$. We now construct a satisfying assignment
for $\varphi^{\rho}\wedge\tau^{\rho}$. We define an assignment $\mu$ as
$\mu(e^{{\left.\kern-1.2pt\rho\right|_{D(e)}}})\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\lambda(e)$
for $e\in E$. It follows by the definition of $\varphi^{\rho}$, respectively
of $\mu$ that $\mu$ satisfies $\varphi^{\rho}$. Now let
$\ell^{\sigma}\in\tau^{\rho}$ be arbitrary but fixed. We can conclude that
there is an arbiter clause $\neg\ell^{\sigma}\vee\neg\sigma\vee\ell$ that is
active with respect to $\tau\cup\rho$. As the clause is active, we know that
$\lambda\vDash\ell$. This means that $\mu\vDash\ell^{\sigma}$. As the literal
was arbitrary, $\mu$ satisfies $\tau^{\rho}$

Now assume that $\varphi\wedge\varphi_{A}\wedge\tau\wedge\rho$ is
unsatisfiable and show that $\varphi^{\rho}\wedge\tau^{\rho}$ is
unsatisfiable. For this purpose we assume that
$\varphi^{\rho}\wedge\tau^{\rho}$ is satisfied by an assignment $\lambda$ and
show that this implies that we can construct a satisfying assignment $\mu$ for
$\varphi\wedge\varphi_{A}\wedge\tau\wedge\rho$. We define $\mu$ as:

$\mu(x)=\begin{cases}\rho(x)&x\in U\\\ \lambda(x^{\sigma})&x\in E\wedge
x^{\sigma}\in\mathit{var}(\varphi^{\rho}\wedge\tau^{\rho})\\\
\tau(x)&x\in\mathbf{dom}(\tau)\\\ \textsc{true}&\text{otherwise}\end{cases}$

This assignment is well-defined as for each $e\in E$ there is maximally one
annotation. Obviously $\mu$ satisfies $\varphi$ \- any clause containing a
universal literal in the same polarity as in $\rho$ is trivially satisfied,
the remaining clauses are satisfied as $\lambda$ satisfies $\varphi^{\rho}$.
We now show that $\mu$ also satisfies ${\varphi}_{A}$. For this purpose let
$\ell^{\sigma}\vee\neg\sigma\vee\neg\ell$ be a clause in ${\varphi}_{A}$. If
$\mu$ satisfies $\ell^{\sigma}$ or $\neg\sigma$ the clause is satisfied, so
assume the opposite—i.e. $\mu\vDash\neg\ell^{\sigma}$ and $\mu\vDash\sigma$.
This means that we have $\rho\vDash\sigma$. Now we have to differentiate
between three cases: If $\mathit{var}(\ell^{\sigma})\in\mathbf{dom}(\tau)$
then we have $\tau\vDash\ell^{\sigma}$, which implies
$\tau^{\sigma}\vDash\ell^{\sigma}$. Thus, as $\lambda$ satisfies
$\tau^{\sigma}$ we know that $\mu\vDash\neg\ell$. If
$\mathit{var}(\ell^{\sigma})\notin\mathbf{dom}(\tau)$ and
$\mathit{var}(\ell^{\sigma})\in\mathit{var}(\varphi^{\rho}\wedge\tau^{\rho})$
then $\mu(\ell)=\mu(\ell^{\sigma})$. If
$\mathit{var}(\ell^{\sigma})\notin\mathbf{dom}(\tau)$ and
$\mathit{var}(\ell^{\sigma})\notin\mathit{var}(\varphi^{\rho}\wedge\tau^{\rho})$
we have $\mu(\mathit{var}(\ell))=\mu(var(\ell^{\sigma}))=\textsc{true}$. To
sum up this means that $\mu$ satisfies the arbiter clause. As the arbiter
clause was arbitrary we thus know that $\mu$ satisfies
$\varphi\wedge{\varphi}_{A}\wedge\tau\wedge\rho$. But this is a contradiction.
Thus, we have shown that $\varphi^{\rho}\wedge\tau^{\rho}$ is unsatisfiable.

###### Remark 3

Let $\pi$ be a refutation of a formula $\varphi$. Additionally, let
$C_{1},C_{2}$ and $C$ be clauses in $\pi$ such that $C$ is the result of
resolving $C_{1}$ and $C_{2}$ with respect to a pivot $x$. We denote the
clause $C$ by $\mathcal{R}_{x}(C_{1},C_{2})$.

###### Lemma 5

Let $\varphi$ be a formula and $L=\\{\ell_{1},\cdots,\ell_{n}\\}$ be a set of
literals with pairwise different variables. If $\varphi\wedge L$ is
unsatisfiable and for each $\hat{L}\subsetneq L$ the formula
$\varphi\wedge\hat{L}$ is satisfiable then the clause
$\neg\ell_{1}\vee\ldots\vee\neg\ell_{n}$ can be derived from $\varphi$ by
resolution.

###### Proof

Let $\hat{\varphi}$ be the clause which is the result of removing all clauses
from $\varphi$ which are subsumed by a literal in $L$. Now we can conclude the
following properties:

  * •

$\hat{\varphi}\wedge L$ is unsatifiable.

  * •

For each $\hat{L}\subsetneq L$ the formula $\hat{\varphi}\wedge\hat{L}$ is
satisfiable.

  * •

Let $\ell\in L$ then $\ell$ does not occur in $\hat{\varphi}$.

As resolution is refutationally complete we can conclude with the above
properties that there is a refutation $\pi=\pi_{1},\ldots,\pi_{m}$ for
$\hat{\varphi}\wedge L$. Next we define the relation $\rightarrow$. For this
purpose let $a\in\pi$ and $b\in\pi$ then we define $a\rightarrow b$ if there
is a clause $c\in\pi$ and a variable $x$ such that $b=\mathcal{R}_{x}(a,c)$.
We denote the transitive closure of $\rightarrow$ by $\rightarrow^{\ast}$. Now
we can see that for each $\ell\in L$ we have
$\ell\rightarrow^{\ast}\pi_{m}$—otherwise we would get a contradiction to the
minimality of $L$.

Subsequently, we construct a derivation $\pi^{\prime}$ from $\pi$. For $1\leq
i\leq m$ we define $\pi_{i}^{\prime}$ as:

$\pi^{\prime}_{i}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\pi_{i}\cup\\{\neg\ell\mid\ell\in
L,\ell\rightarrow^{\ast}\pi_{i}\\}$

As the only possibility for a resolution with a pivot in $L$ are resolutions
with unit clauses from $L$ we can see that each clause in $\pi^{\prime}$ is
either a clause in $\hat{\varphi}\wedge L$, the result of resolving on
previous elements of $\pi^{\prime}$ or the copy of a previous element of
$\pi^{\prime}$—note to simplify the work with indices we use copies of
clauses. Finally, we can see that
$\pi^{\prime}_{m}=\neg\ell_{1}\vee\ldots\vee\neg\ell_{m}$.

###### Lemma 6

Let $\tau$ be an arbiter assignment and $\rho$ a universal assignment. If
$\varphi^{\rho}\wedge\tau^{\rho}$ is unsatisfiable then a subclause of
$\neg\tau^{\rho}$ is derivable from $\Phi$ in the $\forall$Exp+Res calculus.

###### Proof

As $\varphi^{\rho}\wedge\tau^{\rho}$ is unsatisfiable there is a term
$\hat{\tau}\subseteq\tau$ such that $\varphi^{\rho}\wedge\hat{\tau}^{\rho}$ is
unsatisfiable and such that for each term $t\subset\hat{\tau}$ the formula
$\varphi^{\rho}\wedge\ t^{\rho}$ is satisfiable. This means we can apply Lemma
5, which shows that $\neg\hat{\tau}$ is derivable by resolution from
$\varphi^{\rho}$. As $\varphi^{\rho}$ is obtained by instantiating the matrix
$\varphi$ by the universal assignment $\rho$, we can derive $\neg\hat{\tau}$
in $\forall$Exp+Res from $\Phi$.

Before we now use the above results to show that for each clause that is added
to the arbiter solver we can derive a subclause, we will show that this clause
is well-defined,

###### Lemma 7

If $\neg\varphi\wedge\psi_{\mathit{Def}}\wedge\tau$ is satisfied by an
assignment $\sigma$ then the formula
$\varphi\wedge\varphi_{A}\wedge\tau\wedge{\left.\kern-1.2pt\sigma\right|_{U}}$
is unsatisfiable.

###### Proof

If $\neg\varphi\wedge\psi_{\mathit{Def}}\wedge\tau$ is satisfied by an
assignment $\sigma$, then
$\varphi\wedge\psi_{\mathit{Def}}\wedge\tau\wedge\sigma$ is unsatisfiable. As
$\tau$ uniquely determines the assignment for the arbiter variables and
$\tau$, ${\left.\kern-1.2pt\sigma\right|_{U}}$ and $\psi_{\mathit{Def}}$
unquietly determine the assignment for the existential variables also the
formula
$\varphi\wedge\psi_{\mathit{Def}}\wedge\tau\wedge{\left.\kern-1.2pt\sigma\right|_{U}}$
is unsatisfiable. This implies that the formula
$\varphi\wedge\varphi_{A}\wedge\psi_{\mathit{Def}}\wedge\tau\wedge{\left.\kern-1.2pt\sigma\right|_{U}}$
is unsatisfiable. We can now apply Lemma 2 and conclude that
$\varphi\wedge\varphi_{A}\wedge\tau\wedge{\left.\kern-1.2pt\sigma\right|_{U}}$
is unsatisfiable.

The above lemma implies that the core extraction (line 27) is well-defined.

######  Proposition 1 ()

For each clause $C$ added to the arbiter solver by Algorithm 1 (line 28), a
clause $C^{\prime}\subseteq C$ can be derived from $\Phi$ in $\forall$Exp+Res.

###### Proof

By applying the Lemmata 4 and 6 we can conclude that a subclause of
$\neg\tau^{{\left.\kern-1.2pt\sigma\right|_{U}}}$ is derivable from $\Phi$. As
$\neg\tau^{{\left.\kern-1.2pt\sigma\right|_{U}}}$ is a subclause of $\neg\tau$
we have proven the lemma.

###### Theorem 3.2

If Algorithm 1 returns false for the DQBF $\Phi$ then $\Phi$ is false.

###### Proof

If the algorithm returns false then the set $\mathcal{C}$ of clauses in the
arbiter solver is unsatisfiable. By Proposition 1 for each $C\in\mathcal{C}$
we can derive a clause $C^{\prime}\subseteq C$ subsuming $C$ in
$\forall$Exp+Res, so there is a $\forall$Exp+Res refutation of $\Phi$. As
$\forall$Exp+Res is sound [6], this shows that $\Phi$ is false.

Finally, Algorithm 1 terminates since at most one arbiter variable is
introduced for each existential variable and assignment of its dependency set
in the first phase, and there is a limited number of clauses on arbiter
variables that can be introduced in the second phase. In combination with
Theorem 3.1 and Theorem 3.2, we obtain the following result.

###### Corollary 1

Algorithm 1 is a decision procedure for DQBF.

###  3.2 Combining Definition Extraction with CEGIS

Discounting SAT calls, the running time of Algorithm 1 is essentially
determined by the number of assignments of a dependency set for which the
corresponding existential variable is not defined: it introduces an arbiter
variable for each such assignment in the first phase, and the number of
iterations in the second phase is bounded by the number of arbiter
assignments. As a result, even a single existential variable that is
unconstrained and has a large dependency set causes the algorithm to get stuck
enumerating universal assignments.

A key insight underlying the success of counter-example guided solvers for QBF
[26, 25, 46] is that it is typically overkill to perform complete expansion of
universal variables. Instead, they incrementally refine Skolem functions by
taking into account universal assignments that pose a problem for the current
solution candidate.222In these QBF solvers, Skolem functions are typically
only indirectly represented by trees of formulas (_abstractions_) that encode
viable assignments.

Following this idea, we now present an improved algorithm (Algorithm 2) in the
style of Counter-Example Guided Inductive Synthesis (CEGIS) [28]. It
integrates the two phases of Algorithm 1 into a single loop. In each
iteration, it first tries to find definitions for existential variables in
terms of their dependency sets and the arbiter variables (FindDefinitions).
The algorithm then proceeds to a validity check of the definitions under the
current arbiter assignment (CheckArbiterAssignment). A key difference to
Algorithm 1 is that we may not have a definition for each variable at this
point. In this case, we can simply leave the existential variable
unconstrained in the SAT call except for arbiter clauses $\varphi_{A}$ (and
_forcing clauses_ $\varphi_{F}$, which we discuss later). In the
implementation, we limit the SAT solver’s freedom to generate counterexamples
by substituting a default value or a heuristically obtained “guess” for the
Skolem function. Here, any function on variables from the dependency set can
be used without affecting correctness, one only has to make sure that
counterexamples are not repeated to guarantee termination.

If a counterexample $\sigma$ is found, procedure CheckArbiterAssignment
returns it to the main loop. Otherwise, (line 26), we have to check whether
the SAT call in line 21 returned UNSAT because a model has been found, or
whether there is an inconsistency in the formula $\varphi_{A}\land\varphi_{F}$
comprised of arbiter and forcing clauses under the current arbiter assignment
$\tau$. The procedure CheckConsistency either finds that the model is
consistent, in which case Algorithm 2 returns true, or else computes an
assignment $\sigma$ of the universal variables as a counterexample. If
CheckArbiterAssignment returns false, the main loop resumes in line 14 with a
call to AnalyzeConflict.

To see what this procedure does, let us first consider the simple case in
which the counterexample $\sigma$ only contains an assignment of universal
variables that was returned by the consistency check. Then, the existential
assignment $\rho_{\exists}=\emptyset$ is empty, the for-loop is skipped and no
new arbiter variables are introduced (line 57), and the procedure only tries
to further simplify the failed arbiter assignment $\rho_{A}$ in line 60,
before adding its negation to the arbiter solver.

Now assume $\rho_{\exists}$ is nonempty but the case distinction in the body
of the for-loop between lines 45 and 56 always leads to line 53. Then
$\mathit{notforced}=\rho_{\exists}$ and the procedure NewArbiters creates new
arbiter variables $A^{\prime}$ and clauses $\varphi_{A}^{\prime}$ for each
existential variable $e\in\mathbf{dom}(\rho_{\exists})$ and the universal
counterexample $\sigma_{\forall}$ (restricted to the dependency set $D(e)$ in
each case). Since these arbiter variables determine the assignment of the
existential variables in $\mathbf{dom}(\rho_{\exists})$ under
$\sigma_{\forall}$, we can replace $\rho_{\exists}$ with the assignment
$\rho_{A}^{\prime}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\\{e^{\xi}\in
A^{\prime}\>|\>e\in\rho_{\exists}\\}\cup\\{\neg e^{\xi}\in A^{\prime}\>|\>\neg
e\in\rho_{\exists}\\}$ (line 59) and conclude that
$\varphi\land\varphi_{A}\land\varphi_{F}$ is unsatisfiable under the
assignment $\rho_{A}\cup\rho_{A}^{\prime}\cup\sigma_{\forall}$, which only
assigns arbiter variables and universal variables. A clause forbidding the
arbiter assignment $\rho_{A}\cup\rho_{A}^{\prime}$ can now be added as before.

Finally, let us turn to the general case, which includes entailment checks for
each existential literal $\ell\in\rho_{\exists}$ in the minimized
counterexample. These checks are added to reduce the number of new arbiter
variables created. If the literal $\ell$ is entailed by the assignment
$\sigma_{\forall}\land\tau$, we add further literals from $\tau$ to the failed
arbiter assignment $\rho_{A}$ (if necessary) to ensure that $\ell$ is entailed
by $\sigma_{\forall}\land\rho_{A}$. No arbiter variable has to be introduced
for $\mathit{var}(\ell)$ in this case. Otherwise, if $\neg\ell$ is entailed by
$\sigma_{\forall}\land\tau$, then the counterexample is spurious since
$e=\mathit{var}(\ell)$ must be assigned the opposite way under
$\sigma_{\forall}\land\tau$ by any Skolem function. To enforce this in the
next iteration, the algorithm adds a _forcing clause_ $C$ encoding the
implication $\sigma_{\forall}\land\tau\rightarrow\neg\ell$ (which can be
further strengthened by restricting $\sigma_{\forall}$ to the dependency set
of $e$) to $\varphi_{F}$. It also sets a flag $\mathit{oppositeForced}$, which
causes AnalyzeConflict to exit with true instead of adding new arbiter
variables.

If AnalyzeConflict returns true, Algorithm 2 proceeds to the next iteration of
its main loop with the same arbiter assignment $\tau$ but additional forcing
clauses. Otherwise, AnalyzeConflict returns false after adding a clause to the
SAT solver $\mathit{arbiterSolver}$, and FindNewArbiterAssignment is called to
determine a new arbiter assignment $\tau$ that satisfies all previously added
clauses. Algorithm 2 terminates either when it discovers a model or when it
cannot find a new arbiter assignment.

Algorithm 2 Solving DQBF by Definition Extraction (CEGIS Version)

1:procedure SolveByDefinitionExtractionCEGIS($\Phi$)

2: $\triangleright$ $\Phi=\forall u_{1}\ldots\forall u_{n}\exists
e_{1}(D_{1})\ldots\exists e_{m}(D_{m}).\varphi$

3: $\triangleright$ $A$: arbiter variables, $\psi_{\mathit{Def}}$:
definitions, $\varphi_{A}$: arbiter clauses

4:
$A\leftarrow\emptyset,\,\psi_{\mathit{Def}}\leftarrow\emptyset,\,\varphi_{A}\leftarrow\emptyset$

5: $\varphi_{F}\leftarrow\emptyset$ $\triangleright$ forcing clauses

6: $\tau\leftarrow\emptyset$$\triangleright$ arbiter assignment

7: $\mathit{arbiterSolver}\leftarrow\textsc{SatSolver}(\emptyset)$

8: loop

9: $\psi_{\mathit{Def}}\leftarrow\textsc{FindDefinitions}(\\{e\in
E\>|\>e\text{ undefined}\\},\varphi\wedge\varphi_{A}\wedge\varphi_{F})$

10:
$\mathit{modelValid},\sigma\leftarrow\textsc{CheckArbiterAssignment}(\tau)$

11: if $\mathit{modelValid}$ then

12: return true

13: $\triangleright$ $\sigma$ is a counterexample

14: if $\textsc{AnalyzeConflict}(\sigma)$ then

15: $\triangleright$ forcing clauses have been added to $\varphi_{F}$

16: continue

17: if not $\textsc{FindNewArbiterAssignment}($) then

18: return false

19:

20:procedure CheckArbiterAssignment($\tau$)

21:
$\mathit{checker}\leftarrow\textsc{SatSolver}(\neg\varphi\wedge\psi_{\mathit{Def}}\wedge\varphi_{F}\wedge\varphi_{A})$

22: if $\mathit{checker}.\textsc{solve}(\tau)$ then

23: $\sigma\leftarrow\mathit{checker}.\textsc{values}(E\cup U)$

24: return false, $\sigma$

25: else

26:
$\mathit{isConsistent},\sigma\leftarrow\textsc{CheckConsistency}(\varphi_{A}\wedge\varphi_{F},\tau)$

27: if $\mathit{isConsistent}$ then

28: return true, $\emptyset$

29: else

30: $\triangleright$ $\sigma\in[U]$ is such that
$\varphi_{A}\land\varphi_{F}\land\tau\land\sigma$ is unsatisfiable

31: return false, $\sigma$

32:

33:procedure FindNewArbiterAssignment()

34: if $\mathit{arbiterSolver}.\textsc{Solve}($) then

35:
$\tau\leftarrow{\left.\kern-1.2pt\mathit{arbiterSolver}.\textsc{getModel}(\right)|_{A}}$

36: return true

37: return false

38:procedure AnalyzeConflict($\sigma$)

39: $\sigma_{\forall}\leftarrow{\left.\kern-1.2pt\sigma\right|_{U}}$
$\triangleright$ $\sigma_{\forall}$ assigns _all_ universal variables

40:
$\rho\leftarrow\textsc{getCore}(\varphi\wedge\varphi_{A}\wedge\varphi_{F},\sigma\wedge\tau)$

41: $\rho_{\exists}\leftarrow{\left.\kern-1.2pt\rho\right|_{E}}$,
$\rho_{A}\leftarrow{\left.\kern-1.2pt\rho\right|_{A}}$

42: $\mathit{notForced}\leftarrow\emptyset$ $\triangleright$ collect literals
$\ell\in\rho_{\exists}$ that are not implied

43: $\mathit{oppositeForced}\leftarrow$ false

44: $\psi\leftarrow\varphi\wedge\varphi_{A}\wedge\varphi_{F}$

45: for $\ell\in\rho_{\exists}$ do

46: if $\psi\wedge\sigma_{\forall}\wedge\tau\models\ell$ then

47:
$\rho\leftarrow\textsc{getCore}(\psi,\sigma_{\forall}\wedge\tau\wedge\neg\ell)$

48: $\rho_{A}\leftarrow\rho_{A}\cup{\left.\kern-1.2pt\rho\right|_{A}}$
$\triangleright$ add reason for $\ell$ to failed arbiter assignment $\rho_{A}$

49: else if $\psi\wedge\sigma_{\forall}\land\tau\models\neg\ell$ then

50:
$\varphi_{F}\leftarrow\varphi_{F}\wedge\textsc{getForcingClause}(\psi,\sigma_{\forall}\wedge\tau,\neg\ell)$

51: $\mathit{oppositeForced}\leftarrow\textsc{true}$

52: else

53: $\mathit{notForced}\leftarrow\mathit{notForced}\cup\\{\ell\\}$

54: if $\mathit{oppositeForced}$ then

55: return true

56: $\triangleright$ no literal was forced to the opposite polarity

57:
$\varphi_{A}^{\prime},A^{\prime}\leftarrow\textsc{newArbiters}(\mathit{notForced},\sigma_{\forall})$

58: $\varphi_{A}\leftarrow\varphi_{A}\land\varphi_{A}^{\prime}$

59:
$\rho_{A}\leftarrow\rho_{A}\wedge\textsc{setAssignment}(A^{\prime},\rho_{\exists})$

60:
$\rho_{A}\leftarrow{\left.\kern-1.2pt\textsc{getCore}(\psi,\rho_{A}\land\sigma_{\forall})\right|_{A}}$

61: $\mathit{arbiterSolver}.\textsc{addClause}(\neg\rho_{A})$

62: return false

We now prove that Algorithm 2 is a decision procedure for DQBF. As some of the
required proofs are similar to related proofs in the previous section we will
not give all the details.

As in Section 3.1, $A$ denotes a set of arbiter variables and $\varphi_{A}$
denotes the associated set of arbiter clauses. Additionally, $\psi$ denotes
some formula with variables in $U\cup E\cup A$.

Several proofs given in this section build on related proofs given in Section
3.1. As several properties can be proven similarly as related properties in
Section 3.1 we will sometimes give no proof, respectively only a sketch of a
proof.

######  Definition 3 (Forcing Clause)

Let $\ell$ be an existential literal, $\psi$ a formula with
$\mathit{var}(\psi)\subseteq U\cup E\cup A$ and let $\sigma$ be a (partial)
assignment for $U\cup A$. We say that $\ell$ is _forced_ by $\sigma$ in $\psi$
if $\psi\wedge\sigma\wedge\neg\ell$ is unsatisfiable. If $\ell$ is forced by
$\sigma$ then $\neg{\left.\kern-1.2pt\sigma\right|_{D(\mathit{var}(\ell))\cup
A}}\vee l$ is a _forcing clause_.

In particular, if a literal $\ell$ is forced by an assignment $\sigma$ in a
formula $\varphi$ then $\varphi\wedge\sigma\vDash\ell$ holds.

###### Remark 4

We can see that if a literal is forced then it keeps being forced after the
addition of a clause.

###### Lemma 8

Let $\neg p\vee\ell$ be a forcing clause for $\ell$ in $\psi$. Then there is
no model $F$ for $\mathcal{Q}\exists A(\emptyset).\psi$ such that:

  * •

For every arbiter literal $a\in p$ the model function $F_{\mathit{var}(a)}$
satisfies $a$.

  * •

For some assignment $\sigma\in[D(\mathit{var}(\ell))]$ with
$\sigma\vDash{\left.\kern-1.2ptp\right|_{U}}$ the assignment
$F_{\mathit{var}(\ell)}(\sigma)$ satisfies $\neg\ell$.

###### Proof

As $\neg p\vee\ell$ is a forcing clause we know that there is a partial
assignment $\rho$ for $U\cup A$ such that
$p={\left.\kern-1.2pt\rho\right|_{D(\mathit{var}(\ell))\cup A}}$ and
$\psi\wedge\rho\wedge\neg\ell$ is unsatisfiable. Now let $F$ be a model with
the above properties and $\sigma$ as in the second property. Furthermore, let
$\sigma^{\prime}\in[U]$ such that $\sigma\subseteq\sigma^{\prime}$ and such
that for each $x\in\mathbf{dom}(\rho)\cap(U\setminus D(\mathit{var}(\ell)))$
we have $\sigma^{\prime}(x)=\rho(x)$. As $\sigma^{\prime}\cup
F(\sigma^{\prime})$ satisfies $\rho\wedge\neg\ell$ we can conclude that
$\sigma^{\prime}\cup F(\sigma^{\prime})$ falsifies $\psi$. This means that $F$
is not a model.

###### Lemma 9

Let $\Psi$ be a DQBF with
$\Psi\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\mathcal{Q}\exists
A(\emptyset).\psi$ and let $\neg p\vee\ell$ be a forcing clause in $\psi$.
Moreover, let
$\Psi^{\prime}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\mathcal{Q}\exists
A.\psi\wedge(\neg p\vee\ell)$. Then $F$ is a model for $\Psi$ if and only if
$F$ is a model for $\Psi^{\prime}$.

###### Proof

If $F$ is a model for $\Psi^{\prime}$ then it is necessarily also a model for
$\Psi$. Thus, it suffices to only consider the other direction of the proof.
Now assume that $F$ is a model for $\Psi$ but not for $\Psi^{\prime}$ and show
a contradiction. As $F$ is not a model for $\Psi^{\prime}$ there must be an
assignment $\sigma$ for the universal variables such that $\sigma\cup
F(\sigma)$ falsifies $\neg p\vee\ell$. Now we can see that $F$ satisfies the
properties given in Lemma 8. This means that $F$ is not a model for $\Psi$.
This proofs the lemma.

An immediate consequence of the above lemma is the following corollary.

###### Corollary 2

Let $C=\neg p\vee\ell$ be a forcing clause in $\psi$. Then $\mathcal{Q}\exists
A.\psi\wedge C$ is true if and only if $\mathcal{Q}\exists A.\psi$ is true.

The above results imply that forcing clauses can be added to the matrix of a
DQBF without changing its models. In particular, the resulting DQBF has the
same truth value.

###### Lemma 10

Let $\Phi^{\prime}$ be the DQBF
$\Phi^{\prime}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\mathcal{Q}\exists
A(\emptyset).\varphi\wedge\varphi_{A}$. Then, $\Phi$ is true if and only if
$\Phi^{\prime}$ is true.

###### Proof

We assume that $\Phi$ is true. This means that there is a model function
$f_{e}$ in $\Phi$ for each existential variable $e$. We now construct model
functions $f^{\prime}_{e}$ for $\Phi^{\prime}$ by:

$f^{\prime}_{x}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\begin{cases}f_{x}&\text{for
}x\in E\\\ f_{e}(\sigma)&\text{for }x=e^{\sigma}\end{cases}$

Obviously the model given above satisfies $\varphi$ for all assignments to the
universal variables. Now assume that there is a universal assignment $\rho$
such that a clause $\ell^{\sigma}\vee\neg\sigma\vee\neg\ell$ in $\varphi_{A}$
is falsified under the above model. Let $e=\mathit{var}(\ell)$ then it
suffices to consider the case ${\left.\kern-1.2pt\rho\right|_{D(e)}}=\sigma$.
Moreover, we can assume that $f_{e}$ satisfies $\ell$ under $\sigma$—otherwise
the clause would be satisfied. The above assumptions imply that
$f_{e^{\sigma}}\vDash\ell^{\sigma}$. But this yields a contradiction to the
initial assumption. As the above clauses were arbitrary we can conclude that
$\varphi\wedge\varphi_{A}$ is satisfied by the model under each universal
assignment.

Now assume that $\Phi^{\prime}$ is true. We can see that by restricting a
model of $\Phi^{\prime}$ to the variables in $E$ we get a model for $\Phi$.
This proves the equivalence.

By combining the above results we can derive the following corollary.

###### Corollary 3

Let $C_{1},\ldots,C_{k}$ be clauses such that for each index $i$, the clause
$C_{i}$ is a forcing clause in $\varphi\wedge\varphi_{A}\wedge\bigwedge_{1\leq
j<i}C_{j}$. Then the DQBF $\mathcal{Q}\exists
A(\emptyset).\varphi\wedge\varphi_{A}\wedge\bigwedge_{1\leq i\leq k}C_{i}$ is
true if and only if $\Phi$ is true.

Subsequently, we will give a mild generalization of Lemma 3. As this Lemma can
be proven similarly as Lemma 3 we do not give a proof.

###### Lemma 11

Assume there is a linear ordering for $E$, denoted by $<_{E}$. If there is a
set $E^{\prime}\subseteq E$ such that there is a formula $\psi_{e}$ with
$\mathit{var}(\psi_{e})\subseteq D(e)\cup\\{x\in E\mid D(x)\subseteq
D(e),x<_{E}e\\}$ such that $\neg\varphi\wedge\bigwedge_{e\in
E}(e\leftrightarrow\psi_{e})$ is unsatisfiable then the DQBF $\Phi$ is true.

###### Theorem 3.3

If Algorithm 2 returns true for a DQBF $\Phi$ then $\Phi$ is true.

###### Proof

We assume that the algorithm returns true and show that the DQBF $\Phi$ is
true. We know that we have a set $A$ of arbiter variables, a set $\varphi_{A}$
of arbiter clauses, a set $\varphi_{F}$ of forcing clauses and a set
$E^{\prime}\subseteq E$ such that each $e\in E^{\prime}$ has a definition
$\psi_{e}$ in $\varphi\wedge\varphi_{A}\wedge\varphi_{F}$ by $D(e)\cup A$. Let
$\psi_{\mathit{Def}}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\bigwedge_{e\in
E^{\prime}}(e\leftrightarrow\psi_{e})$ and
$\Phi^{\prime}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\mathcal{Q}\exists
A(\emptyset).\varphi\wedge\varphi_{A}\wedge\varphi_{F}$. By Corollary 3, we
know that $\Phi$ is true if and only if $\Phi^{\prime}$ is true. As the
algorithm returns true, we know that
$\neg\varphi\wedge\varphi_{A}\wedge\varphi_{F}\wedge\psi_{\mathit{Def}}$ is
unsatisfiable. By Lemma 11 and the above property we know that $\Phi^{\prime}$
is true. Thus, $\Phi$ is true as well.

###### Lemma 12

Let $\varphi_{F}$ be a set of forcing clauses, $\sigma$ be an assignment for
universal variables and $\tau\in[A]$. If
$\varphi\wedge\varphi_{A}\wedge\varphi_{F}\wedge\tau\wedge\sigma$ is
unsatisfiable then we can derive a subclause of $\neg\tau^{\sigma}$ from
$\Phi$ in $\forall$Exp+Res.

###### Proof

If $\varphi\wedge\varphi_{A}\wedge\tau\wedge\sigma$ is unsatisfiable then the
result follows by Lemma 4 and Lemma 6. We can now assume that
$\varphi\wedge\varphi_{A}\wedge\tau\wedge\sigma$ is satisfied by an assignment
$\rho$. Now there has to be a forcing clause $(\neg p\vee\ell)$ that is
falsified by $\rho$ such that the set of forcing clauses $\hat{\varphi}_{F}$
that were introduced before $(\neg p\vee\ell)$, is satisfied by $\sigma$—note
$(\neg p\vee\ell)$ is a forcing clause for
$\varphi\wedge\varphi_{A}\wedge\hat{\varphi}_{F}$. As $\rho$ falsifies $\neg
p$ it satisfies $p$, as $\rho$ additionally satisfies $\tau$ we can conclude
that the arbiter literals in $p$ are contained in $\tau$ Subsequently,
$v_{i},\ldots,v_{k}$ shall denote the universal literals in $p$ and
$\ell_{1}^{\sigma_{1}},\ldots,\ell_{l}^{\sigma_{l}}$ the arbiter literals in
$p$. Moreover, $\Phi^{\prime}$ shall denote the DQBF
$\Phi^{\prime}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\mathcal{Q}\exists
A(\emptyset).\varphi\wedge\varphi_{A}\wedge\hat{\varphi}_{F}$. Because, of the
above property $\Phi^{\prime}$ cannot have a model $F$ with
$F\vDash\bigwedge\ell_{i}^{\sigma_{i}}$ and
$F({\left.\kern-1.2pt\rho\right|_{U}})\vDash\ell$. On the other hand because
of Lemma 8 there can also be no model with
$F\vDash\bigwedge\ell_{i}^{\sigma_{i}}$ and
$F({\left.\kern-1.2pt\rho\right|_{U}})\vDash\neg\ell$. This means that if
$\Phi^{\prime}$ has a model than it has to falsify
$\bigwedge\ell_{i}^{\sigma_{i}}$. We know that adding forcing clause to a
matrix does not change models. Thus, if
$\Phi^{\prime\prime}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\mathcal{Q}\exists
A(\emptyset).\varphi\wedge\varphi_{A}$ has a model $F$ than it has to falsify
$\bigwedge\ell_{i}^{\sigma_{i}}$. This means that there is some minimal subset
$S$ of $\\{\ell_{1}^{\sigma_{1}},\ldots,\ell_{l}^{\sigma_{l}}\\}$ such that
$\mathcal{Q}\exists A(\emptyset).\varphi\wedge\varphi_{A}\wedge\bigwedge S$ is
false. Now let $\varphi_{A}^{S}$ be the subset of $\varphi_{A}$ with arbiters
in $S$. We show that
$\hat{\Phi}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\mathcal{Q}\exists
A(\emptyset).\varphi\wedge\varphi_{A}^{S}\wedge\bigwedge S$ is false. We
assume the opposite. In this case there is a model for the formula. But such a
model can easily be extended to a model for $\Phi^{\prime\prime}$, which
yields a contradiction.

Next we argue that
$\tilde{\Phi}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\mathcal{Q}.\varphi\wedge\bigwedge\\{\neg\sigma\vee\ell\mid\ell^{\sigma}\in
S\\}$ is false. Again, assume the opposite, i.e. there is a model $F$. We now
show that that this model can be extended to a model $F^{\prime}$ for
$\hat{\Phi}$. Now let $\ell^{\sigma}\in S$, we set
$F_{\mathit{var}(\ell^{\sigma})}=F_{\mathit{var}(\ell)}(\sigma)$. We can see
that $F^{\prime}$ is a model for $\hat{\Phi}$, but this is a contradiction.
Moreover, by using similar arguments as above we can show that for any subset
$S^{\prime}$ of $S$ the formula
$\mathcal{Q}.\varphi\wedge\bigwedge\\{\neg\sigma\vee\ell\mid\ell^{\sigma}\in
S^{\prime}\\}$ is true.

Now let $C$ denote the set of clause that represent the full expansion of
$\tilde{\Phi}$—in the sense of $\forall$Exp+Res. As $\tilde{\Phi}$ is false,
there is a $\forall$Exp+Res proof. This means there is a refutation by
resolution for $C$. We can now on the one hand see that $S\subseteq C$ and on
the other hand, because of the minimality of $S$ that removing any element
from $S$ from $C$ would make $C$ satisfiable. By Lemma 6 we can now conclude
that we can derive
$\overline{S}\mathrel{\vbox{\hbox{\scriptsize.}\hbox{\scriptsize.}}}=\\{\neg
x\mid x\in S\\}$ by resolution from $C$. From this we can conclude that
$\overline{S}$ is derivable from $\Phi$ in $\forall$Exp+Res. As $\overline{S}$
is a subset of $\neg\tau$ this proves the lemma.

As in the case of Algorithm 1, the correctness of false answers for Algorithm
2 follows from a correspondence with $\forall$Exp+Res derivations. Before we
prove that each clause that is added to the arbiter solver correponds to a
clause that can be derived by $\forall$Exp+Res we show that the clauses that
are added to the arbiter solver are well-defined.

###### Lemma 13

The core extraction in line 40 is well defined.

###### Proof

We have to show that $\psi\wedge\rho_{A}\wedge\sigma_{\forall}$ is indeed
unsatisfiable. There are two cases to consider. First assume that
$\varphi_{A}\wedge\varphi_{F}$ was inconsistent under $\tau$ and
$\sigma_{\forall}$. The inconsistency means that
$\varphi_{A}\wedge\varphi_{F}\wedge\tau\wedge\sigma_{\forall}$ is
unsatisfiable. This means that the core extraction is well-defined. In the
second case the formula
$\neg\varphi\wedge\psi_{\mathit{Def}}\wedge\varphi_{F}\wedge\varphi_{A}\wedge\tau$
was satisfied by $\sigma\cup\tau$. This means that
$\varphi\wedge\psi_{\mathit{Def}}\wedge\varphi_{F}\wedge\varphi_{A}\wedge\varphi_{A}^{\prime}\wedge\sigma\wedge{\left.\kern-1.2pt\rho\right|_{A}}$
is unsatisfiable—where $\varphi_{A}^{\prime}$ denotes the arbiter clauses that
were introduces in this step. By Lemma 2 the formula
$\varphi\wedge\varphi_{F}\wedge\varphi_{A}\wedge\varphi_{A}^{\prime}\wedge\sigma\wedge{\left.\kern-1.2pt\rho\right|_{A}}$
is unsatisfiable. Moreover, we can argue that
$\varphi\wedge\psi_{\mathit{Def}}\wedge\varphi_{F}\wedge\varphi_{A}\wedge\varphi_{A}^{\prime}\wedge{\left.\kern-1.2pt\sigma\right|_{U}}$
is unsatisfiable—the existential assignments in $\sigma$ are either forced or
ruled out by the new arbiter clauses. Finally, by similar arguments as in
previous proofs, also removing $\psi_{\mathit{Def}}$ does preserve
unsatisfiability. This shows that also in this case the core extraction is
well-defined.

######  Proposition 2 ()

For each clause $C$ added to the arbiter solver by Algorithm 2 (line 61), a
clause $C^{\prime}\subseteq C$ can be derived from $\Phi$ in $\forall$Exp+Res.

###### Proof

Let $\neg\rho_{A}$ be a clause that is added to the arbiter solver. Then we
know that
$\varphi\wedge\varphi_{A}\wedge\varphi_{F}\wedge\rho_{A}\wedge\sigma$ for some
universal assignment $\sigma$ is unsatisfiable. By applying Lemma 12 we can
conclude that we can derive a subset of $\neg\rho_{A}$.

######  Theorem 3.4 ()

If Algorithm 2 returns false for a DQBF $\Phi$ then $\Phi$ is false.

###### Proof

If the algorithm returns false then the clauses in the
$\mathit{arbiterSolver}$ are unsatisfiable. Subsequently, we denote those
clauses by $\mathcal{C}$. By Proposition 2, we know that we can derive for
each clause $C\in\mathcal{C}$ a subclause. This means that those derivable
clauses are unsatisfiable. As propositional resolution is refutationally
complete we can derive the empty clause from those derivable clauses. This
means that there is a $\forall$Exp+Res proof for $\Phi$. As $\forall$Exp+Res
is sound, this means that $\Phi$ is false.

Each iteration of Algorithm 2 introduces new forcing clauses or forbids
another arbiter assignment. Because there is a bound on the number of arbiter
variables that can be introduced, the number of such clauses can be bounded as
well, and the algorithm eventually terminates. Together with Theorem 3.3 and
Theorem 3.4, this gives rise to the following corollary.

###### Corollary 4

Algorithm 2 is a decision procedure for DQBF.

##  4 Experiments

We implemented Algorithm 2 as described in the previous section in a prototype
named Pedant.333Available at https://github.com/perebor/pedant-solver. For
definition extraction, it uses a subroutine from Unique [40] that in turn
relies on an interpolating version of MiniSat [12] bundled with the ExtAvy
model checker [22, 48]. Further, CaDiCaL is used as a SAT solver [8] (we also
tested with CryptoMiniSAT [44] and Glucose [2] but saw no significant
differences in overall performance). Pedant can read DQBF in the standard
DQDIMACS format and output models in the DIMACS format.

The implementation incorporates a few techniques not explicitly mentioned in
the above pseudocode. We identify _unate_ existential literals (a
generalization of pure literals) [1], which can be used in any model of a
DQBF. Moreover, we set a (configurable) default value for existential
variables that applies when there is no forcing clause propagating a different
value. This is to limit the freedom of the SAT solver used in the validity
check in coming up with counterexamples. Moreover, when checking for
definability of an existential variable, we use _extended dependencies_ that
include existential variables with dependency sets that are contained in the
dependencies of the variable that is checked.

For all experiments described below we use a cluster with Intel Xeon E5649
processors at 2.53 GHz running 64-bit Linux.

###  4.1 Performance on Standard Benchmark Sets

We compare Pedant with other DQBF solvers on standard benchmark sets in terms
of instances solved within the timeout and their PAR2 score.444The Penalized
Average Runtime (PAR) is the average runtime, with the time for each unsolved
instance calculated as a constant multiple of the timeout. Specifically, we
choose the solvers dCAQE [47], iDQ [16], HQS [20], and the recently introduced
DQBDD [39]. Both HQS and DQBDD internally use HQSPre [51] as a preprocessor.
For dCAQE and iDQ, we call HQSPre with a time limit of $300$ seconds (the time
for preprocessing is included in the total running time). By default, Pedant
is run without preprocessing.

The results are based on a single run with a time and memory limit of $1800$
seconds and $8$ GB, respectively, which are enforced using RunSolver
[36].555Due to the heavy-tailed runtime distribution of DQBF solvers, run-to-
run variance rarely affects the number of solved instances. However, PAR2
scores should be taken with a grain of salt and only used to compare orders of
magnitude. We report results for two benchmark sets. The first—which we refer
to as the “Compound” set—has been used in recent papers on HQS [18]. It is
comprised of instances encoding partial equivalence checking (PEC) [37, 16,
19, 14] and controller synthesis [10], as well as succinct DQBF
representations of propositional satisfiability [4]. Results are summarized in
Table 1. Pedant solved the most instances overall and for 4 out of 5 families
(the “Balabanov” family being the exception), with DQBDD coming in a close
second. The performance of Pedant on the PEC instances in the “Finkbeiner”
family is particularly encouraging.

Table 1:  Results for the “Compound” benchmark set.

| dCAQE | DQBDD | HQS | iDQ | Pedant
---|---|---|---|---|---
Family(Total) | Sol/ | PAR2 | Sol/ | PAR2 | Sol/ | PAR2 | Sol/ | PAR2 | Sol/ | PAR2
Balabanov(34) |  21/ | $1.5\\!\cdot\\!10^{3}$ | 13/ | $2.3\\!\cdot\\!10^{3}$ | 19/ | $1.8\\!\cdot\\!10^{3}$ |  21/ | $1.5\\!\cdot\\!10^{3}$ | 13/ | $2.3\\!\cdot\\!10^{3}$
Biere(1200) |  1200/ | $1.6\\!\cdot\\!10^{-1}$ | 1197/ | $9.0\\!\cdot\\!10^{0}$ |  1200/ | $6.4\\!\cdot\\!10^{-2}$ | 1184/ | $6.6\\!\cdot\\!10^{1}$ |  1200/ | $1.0\\!\cdot\\!10^{-1}$
Bloem(461) | 85/ | $2.9\\!\cdot\\!10^{3}$ | 82/ | $3.0\\!\cdot\\!10^{3}$ | 82/ | $3.0\\!\cdot\\!10^{3}$ | 50/ | $3.2\\!\cdot\\!10^{3}$ |  98/ | $2.9\\!\cdot\\!10^{3}$
Finkbeiner(2000) | 32/ | $3.5\\!\cdot\\!10^{3}$ | 1999/ | $1.1\\!\cdot\\!10^{1}$ | 1799/ | $3.9\\!\cdot\\!10^{2}$ | 6/ | $3.6\\!\cdot\\!10^{3}$ |  2000/ | $1.7\\!\cdot\\!10^{0}$
Scholl(1116) | 568/ | $1.8\\!\cdot\\!10^{3}$ | 793/ | $1.1\\!\cdot\\!10^{3}$ | 676/ | $1.4\\!\cdot\\!10^{3}$ | 345/ | $2.5\\!\cdot\\!10^{3}$ |  854/ | $8.7\\!\cdot\\!10^{2}$
All(4811) | 1906/ | $2.2\\!\cdot\\!10^{3}$ | 4084/ | $5.5\\!\cdot\\!10^{2}$ | 3776/ | $7.9\\!\cdot\\!10^{2}$ | 1606/ | $2.4\\!\cdot\\!10^{3}$ |  4165/ | $4.9\\!\cdot\\!10^{2}$

Next, we consider the instances from the DQBF track of QBFEVAL’20 [33].
Results are shown in Table 2. Here, Pedant falls behind the other solvers,
with the exception of iDQ. In particular, significantly fewer instances from
the “Kullmann” and “Tentrup” families are solved.

For the autarky finding benchmarks in the “Kullmann” family [30], we noticed
that most dependencies can be removed by preprocessing with the reflexive
resolution-path dependency scheme [41, 52]. The resulting instances are much
easier to solve for Pedant, and models can still be validated against the
original DQBFs. In general, we found that preprocessing with HQSPre can have
both positive and negative effects on Pedant. The rightmost columns of Table 2
show results when preprocessing is enabled.666With options \--resolution 1
--univ_exp 0 --substitute 0. Overall, performance is clearly improved, but
fewer instances from the “Bloem” and “Scholl” families are solved. In prior
work, it was observed that preprocessing can destroy definitions [40], and
this appears to be the case here as well.

For the instances from the “Tentrup” family, we discovered that the
performance of Pedant is sensitive to which counterexamples are generated by
CaDiCaL. With the right sequence of counterexamples, false instances can be
refuted quickly, while otherwise the solver is busy introducing arbiter
variables for minor variations of previously encountered cases. Curiously,
this also appears to be the case for true instances. We believe that the
algorithm can be made more robust against such “adversarial” sequences of
counterexamples by achieving better generalization (see Section 6).

Table 2:  Results for the QBFEVAL’20 DQBF benchmark set.

| dCAQE | DQBDD | HQS | iDQ | Pedant | PedantHQ
---|---|---|---|---|---|---
Family(Total) | Sol/ | PAR2 | Sol/ | PAR2 | Sol/ | PAR2 | Sol/ | PAR2 | Sol/ | PAR2 | Sol/ | PAR2
Balabanov(34) |  21/ | $1.5\\!\cdot\\!10^{3}$ | 13/ | $2.3\\!\cdot\\!10^{3}$ | 19/ | $1.8\\!\cdot\\!10^{3}$ |  21/ | $1.5\\!\cdot\\!10^{3}$ | 14/ | $2.3\\!\cdot\\!10^{3}$ | 13/ | $2.4\\!\cdot\\!10^{3}$
Bloem(90) | 31/ | $2.4\\!\cdot\\!10^{3}$ | 32/ | $2.3\\!\cdot\\!10^{3}$ | 33/ | $2.3\\!\cdot\\!10^{3}$ | 14/ | $3.1\\!\cdot\\!10^{3}$ |  37/ | $2.2\\!\cdot\\!10^{3}$ | 25/ | $2.7\\!\cdot\\!10^{3}$
Kullmann(50) | 35/ | $1.1\\!\cdot\\!10^{3}$ |  50/ | $1.5\\!\cdot\\!10^{1}$ | 41/ | $6.9\\!\cdot\\!10^{2}$ |  50/ | $3.4\\!\cdot\\!10^{0}$ | 34/ | $1.3\\!\cdot\\!10^{3}$ | 40/ | $7.3\\!\cdot\\!10^{2}$
Scholl(90) | 52/ | $1.5\\!\cdot\\!10^{3}$ | 78/ | $4.9\\!\cdot\\!10^{2}$ | 77/ | $5.3\\!\cdot\\!10^{2}$ | 15/ | $3.0\\!\cdot\\!10^{3}$ |  82/ | $3.3\\!\cdot\\!10^{2}$ | 65/ | $1.2\\!\cdot\\!10^{3}$
Tentrup(90) | 77/ | $5.5\\!\cdot\\!10^{2}$ |  84/ | $2.8\\!\cdot\\!10^{2}$ | 78/ | $5.1\\!\cdot\\!10^{2}$ | 17/ | $2.9\\!\cdot\\!10^{3}$ | 15/ | $3.0\\!\cdot\\!10^{3}$ |  84/ | $2.9\\!\cdot\\!10^{2}$
All(354) | 216/ | $1.4\\!\cdot\\!10^{3}$ |  257/ | $1.0\\!\cdot\\!10^{3}$ | 248/ | $1.1\\!\cdot\\!10^{3}$ | 117/ | $2.4\\!\cdot\\!10^{3}$ | 182/ | $1.8\\!\cdot\\!10^{3}$ | 227/ | $1.4\\!\cdot\\!10^{3}$

###  4.2 Distribution of Defined Existential Variables

The main design goal for Pedant was to create a solver that benefits from
unique Skolem functions given by propositional definitions. We thus expect
Pedant to do well on instances where a large proportion of existential
variables is defined. Figure 2 shows the distribution of defined existential
variables (i.e., unique Skolem functions) as computed by Unique [40].

Figure 2: Distribution of defined variables by benchmark set and family. For a
given percentage $x_{0}$ on the x-axis, the y-axis shows the fraction of
instances from each benchmark family for which $x_{0}$ percent of existential
variables are defined. For example, the instances in the “Balabanov” family
have no defined variables, while the fraction of defined variables for
instances in the “Finkbeiner” family ranges from $75$% to $100$%.

These definitions are also found by Pedant without the introduction of arbiter
variables. Comparing Table 1 and Table 2 with Figure 2, we see that Pedant
performed better for instance families with a larger fraction of defined
variables. This makes sense: the fewer variables are undefined, the fewer
arbiter variables need to be introduced.

###  4.3 Solution Validation

When running Pedant without preprocessing (the default), we had it trace and
output models in DIMACS format. We implemented a simple workflow for
validating these models in Python 3 using the PySAT library [24]. First, a
simple syntactic check is performed to make sure the encoding of each Skolem
function only mentions variables in the dependency set of the corresponding
variable. Then, a SAT solver is used to verify that substituting the model
$\psi$ for existential variables in the matrix $\varphi$ of the input DQBF is
valid, by testing for each clause $C\in\varphi$ whether $\psi\land\neg C$ is
unsatisfiable (cf. Lemma 3). In this manner, we are able to validate models
for all $648$ true DQBFs in the two benchmark sets that were solved by Pedant
without preprocessing. The maximum validation time was $237$ seconds, with a
mean of $4.3$ seconds and a median of $0.5$ seconds.

The current validation process is intended as a proof of concept. Since models
constructed by Pedant are circuits, we plan to support the AIGER format [9] in
the near future, and provide a workflow along the lines of QBFCert [32].

##  5 Related Work

The DQDPLL algorithm lifts the CDCL algorithm to DQBF [15]. While CDCL solvers
are free to assign variables in any order, in DQBF a variable may be assigned
only after the variables in its dependency set have been assigned. Moreover,
its assignment must not differ between branches in the search tree that agree
on the assignment of the dependency set. In DQDPLL, this is enforced by
temporary _Skolem clauses_ that fix the truth value of a variable for a given
assignment of its dependencies. The solver dCAQE lifts clausal abstraction
from QBF to DQBF [47]. QBF solvers based on abstraction maintain a
propositional formula for each quantifier level that characterizes eligible
moves in the evaluation game. These _abstractions_ are refined by forbidding
moves that are known to result in a loss. Abstractions are linked to each
other through auxiliary variables that indicate which clauses are satisfied at
different levels. dCAQE organizes variables in a dependency lattice that
determines the order in which their abstractions may be solved. This can lead
to variables being assigned after variables that do not appear in their
dependency sets, and additional consistency checks have to be applied to
ensure that Skolem functions do not exploit such spurious dependencies. dCAQE
uses _fork resolution_ as its underlying proof system [34].

Expansion of universal variables can be successively applied to transform a
DQBF into a propositional formula that can be passed to a SAT solver [11]. In
practice, the space requirements of fully expanding a DQBF are prohibitive.
This can be addressed by only expanding some universal variables, as well as
considering only a subset of the clauses generated by expansion. Even though
such approaches degenerate into full expansion in the worst case, they can be
quite effective. The solver iDQ [16] successively expands a DQBF in a
counterexample-guided abstraction refinement (CEGAR) loop. Initially,
universal variables in each clause are expanded separately. Satisfiability of
the resulting propositional formula is checked by a SAT solver. If it is
unsatisfiable, so is the original DQBF. Otherwise, iDQ checks whether any pair
of literals with consistent annotations are assigned different truth values in
the satisfying assignment. If there are no such literals, a model of the DQBF
has been found. Otherwise, clauses containing the corresponding clashing
literals are further expanded. The system is inspired by the _Inst-Gen_
calculus, the proof system underpinning the First-Order solver iProver [29].
Originally designed for the effectively propositional fragment of first-order
logic (EPR), iProver also accepts DQBF as input.

The solver HQS seeks to keep the memory requirements of expansion in check by
operating on And-Inverter Graph (AIG) representations of input formulas [20].
It uses expansion alongside several other techniques to transform a DQBF into
an equivalent QBF and leverage advances in QBF solving [50, 18]. HQS is paired
with a powerful preprocessor named HQSPre that provides an arsenal of
additional simplification techniques [51], including an incomplete but
efficient method for refuting DQBF by reduction to a QBF encoding [14]. HQSpre
is also used in the recently developed solver DQBDD [39], which is similar to
HQS but relies on Binary Decision Diagrams (BDDs) instead of AIGs to represent
formulas and perform quantifier elimination.

Evaluating DQBF is NEXPTIME complete [3] in general, but some tractable
subclasses have been identified in recent work [38, 17].

##  6 Conclusion

We presented a decision algorithm for DQBF that relies on definition
extraction to compute Skolem functions inside a CEGIS loop, and evaluated it
in terms of the prototype implementation Pedant. While the initial results are
very promising, we see significant room for improvement and various directions
to pursue in future research. Generally, the approach works well when Skolem
functions can be computed by definition extraction for a large fraction of
existential variables without introducing too many arbiter variables. During
testing, we encountered multiple instances for which conflict analysis was
occupied dealing with minor variations of a small number of counterexamples.
We believe that this is partly due to arbiter variables being introduced for
_complete_ assignments of dependency sets. Even if the assignment of some
universal variables in the dependency set is irrelevant for a given
counterexample, the newly introduced arbiter variables only deal with the
counterexample as represented by the complete assignment, and each
counterexample obtained by varying the assignment of irrelevant universal
variables requires a new set of arbiter variables. To avoid this, we plan to
experiment with a variant of the algorithm that introduces arbiter variables
for _partial_ assignments [29, 16].

A different approach to generalizing from counterexamples—one that does not
require changes in the underlying proof system—is the use of machine learning.
By predicting the pattern common to a sequence of counterexamples, it is
possible to deal with it wholesale and avoid an exhaustive enumeration [25].
Moreover, recent work on Boolean Synthesis demonstrates the viability of
learning Skolem functions by sampling satisfying assignments [21].

Finally, we plan to explore further applications of interpolation-based
definition extraction within our algorithm. Currently, its use is limited to
existential variables that are defined by their dependency sets in the input
DQBF, or are undefined only in a small number of cases. In addition to that,
one could search for “partial” definitions under assignments of the dependency
set characterized by formulas, or introduce definitions that are valid under
assumptions [35].

#### Acknowledgements

Supported by the Vienna Science and Technology Fund (WWTF) under the grants
ICT19-060 and ICT19-065, and the Austrian Science Fund (FWF) under grant
W1255.

## References

  * [1] Akshay, S., Chakraborty, S., Goel, S., Kulal, S., Shah, S.: What’s hard about boolean functional synthesis? In: CAV (1). Lecture Notes in Computer Science, vol. 10981, pp. 251–269. Springer (2018)
  * [2] Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence. pp. 399–404 (2009)
  * [3] Azhar, S., Peterson, G., Reif, J.: Lower bounds for multiplayer non-cooperative games of incomplete information. Journal of Computers and Mathematics with Applications 41, 957 – 992 (2001)
  * [4] Balabanov, V., Chiang, H.K., Jiang, J.R.: Henkin quantifiers and boolean formulae: A certification perspective of DQBF. Theor. Comput. Sci. 523, 86–100 (2014)
  * [5] Baldoni, R., Coppa, E., D’Elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. 51(3), 50:1–50:39 (2018)
  * [6] Beyersdorff, O., Blinkhorn, J., Chew, L., Schmidt, R.A., Suda, M.: Reinterpreting dependency schemes: Soundness meets incompleteness in DQBF. J. Autom. Reason. 63(3), 597–623 (2019)
  * [7] Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, R. (ed.) Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS ’99, Proceedings. Lecture Notes in Computer Science, vol. 1579, pp. 193–207. Springer (1999)
  * [8] Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020\. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., Järvisalo, M., Suda, M. (eds.) Proc. of SAT Competition 2020 – Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51–53. University of Helsinki (2020)
  * [9] Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. Rep. 11/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)
  * [10] Bloem, R., Könighofer, R., Seidl, M.: Sat-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014. Lecture Notes in Computer Science, vol. 8318, pp. 1–20. Springer (2014)
  * [11] Bubeck, U., Kleine Büning, H.: Dependency quantified Horn formulas: Models and complexity. In: Biere, A., Gomes, C.P. (eds.) Theory and Applications of Satisfiability Testing - SAT 2006. Lecture Notes in Computer Science, vol. 4121, pp. 198–211. Springer (2006)
  * [12] Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. Lecture Notes in Computer Science, vol. 2919, pp. 502–518. Springer (2003)
  * [13] Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017\. Lecture Notes in Computer Science, vol. 10205, pp. 354–370 (2017)
  * [14] Finkbeiner, B., Tentrup, L.: Fast DQBF refutation. In: Sinz, C., Egly, U. (eds.) Theory and Applications of Satisfiability Testing - SAT 2014. Lecture Notes in Computer Science, vol. 8561, pp. 243–251. Springer (2014)
  * [15] Fröhlich, A., Kovásznai, G., Biere, A.: A DPLL algorithm for solving DQBF (2012), http://fmv.jku.at/papers/FroehlichKovasznaiBiere-POS12.pdf, presented at _Workshop on Pragmatics of SAT (POS)_
  * [16] Fröhlich, A., Kovásznai, G., Biere, A., Veith, H.: idq: Instantiation-based DQBF solving. In: Berre, D.L. (ed.) POS-14. Fifth Pragmatics of SAT workshop, a workshop of the SAT 2014 conference, part of FLoC 2014 during the Vienna Summer of Logic, July 13, 2014, Vienna, Austria. EPiC Series in Computing, vol. 27, pp. 103–116. EasyChair (2014)
  * [17] Ganian, R., Peitl, T., Slivovsky, F., Szeider, S.: Fixed-parameter tractability of dependency QBF with structural parameters. In: Calvanese, D., Erdem, E., Thielscher, M. (eds.) Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020. pp. 392–402 (2020)
  * [18] Ge-Ernst, A., Scholl, C., Wimmer, R.: Localizing quantifiers for DQBF. In: Barrett, C.W., Yang, J. (eds.) Formal Methods in Computer Aided Design, FMCAD 2019. pp. 184–192. IEEE (2019)
  * [19] Gitina, K., Reimer, S., Sauer, M., Wimmer, R., Scholl, C., Becker, B.: Equivalence checking of partial designs using dependency quantified boolean formulae. In: IEEE 31st International Conference on Computer Design, ICCD 2013,. pp. 396–403. IEEE Computer Society (2013)
  * [20] Gitina, K., Wimmer, R., Reimer, S., Sauer, M., Scholl, C., Becker, B.: Solving DQBF through quantifier elimination. In: Nebel, W., Atienza, D. (eds.) Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, DATE 2015. pp. 1617–1622. ACM (2015)
  * [21] Golia, P., Roy, S., Meel, K.S.: Manthan: A data-driven approach for boolean function synthesis. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020. Lecture Notes in Computer Science, vol. 12225, pp. 611–633. Springer (2020)
  * [22] Gurfinkel, A., Vizel, Y.: Druping for interpolates. In: FMCAD 2014. pp. 99–106. IEEE (2014)
  * [23] Heule, M.J.H., Järvisalo, M., Suda, M.: SAT competition 2018. J. Satisf. Boolean Model. Comput. 11(1), 133–154 (2019)
  * [24] Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: A Python toolkit for prototyping with SAT oracles. In: SAT. pp. 428–437 (2018)
  * [25] Janota, M.: Towards generalization in QBF solving via machine learning. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18). pp. 6607–6614. AAAI Press (2018)
  * [26] Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1–25 (2016)
  * [27] Janota, M., Marques-Silva, J.: On propositional QBF expansions and q-resolution. In: Järvisalo, M., Gelder, A.V. (eds.) Theory and Applications of Satisfiability Testing - SAT 2013. Lecture Notes in Computer Science, vol. 7962, pp. 67–82. Springer (2013)
  * [28] Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. Acta Informatica 54(7), 693–726 (2017)
  * [29] Korovin, K.: iProver - an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008. Lecture Notes in Computer Science, vol. 5195, pp. 292–298. Springer (2008)
  * [30] Kullmann, O., Shukla, A.: Autarkies for DQCNF. In: Barrett, C.W., Yang, J. (eds.) 2019 Formal Methods in Computer Aided Design, FMCAD 2019. pp. 179–183. IEEE (2019)
  * [31] Meel, K.S., Vardi, M.Y., Chakraborty, S., Fremont, D.J., Seshia, S.A., Fried, D., Ivrii, A., Malik, S.: Constrained sampling and counting: Universal hashing meets SAT solving. In: Darwiche, A. (ed.) Beyond NP, Papers from the 2016 AAAI Workshop. AAAI Workshops, vol. WS-16-05. AAAI Press (2016)
  * [32] Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF - (tool presentation). In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing - SAT 2012. Lecture Notes in Computer Science, vol. 7317, pp. 430–435. Springer (2012)
  * [33] Pulina, L., Seidl, M.: The 2016 and 2017 QBF solvers evaluations (qbfeval’16 and qbfeval’17). Artif. Intell. 274, 224–248 (2019)
  * [34] Rabe, M.N.: A resolution-style proof system for DQBF. In: Gaspers, S., Walsh, T. (eds.) Theory and Applications of Satisfiability Testing - SAT 2017. Lecture Notes in Computer Science, vol. 10491, pp. 314–325. Springer (2017)
  * [35] Rabe, M.N., Seshia, S.A.: Incremental determinization. In: Creignou, N., Berre, D.L. (eds.) Theory and Applications of Satisfiability Testing - SAT 2016. Lecture Notes in Computer Science, vol. 9710, pp. 375–392. Springer (2016)
  * [36] Roussel, O.: Controlling a solver execution with the runsolver tool. J. Satisf. Boolean Model. Comput. 7(4), 139–144 (2011)
  * [37] Scholl, C., Becker, B.: Checking equivalence for partial implementations. In: Proceedings of the 38th Design Automation Conference, DAC 2001. pp. 238–243. ACM (2001)
  * [38] Scholl, C., Jiang, J.R., Wimmer, R., Ge-Ernst, A.: A PSPACE subclass of dependency quantified boolean formulas and its effective solving. In: The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019. pp. 1584–1591. AAAI Press (2019)
  * [39] Síč, J.: Satisfiability of DQBF using binary decision diagrams. Master’s thesis, Masaryk University, Brno, Czech Republic (2020)
  * [40] Slivovsky, F.: Interpolation-based semantic gate extraction and its applications to QBF preprocessing. In: CAV (1). Lecture Notes in Computer Science, vol. 12224, pp. 508–528. Springer (2020)
  * [41] Slivovsky, F., Szeider, S.: Soundness of Q-resolution with dependency schemes. Theor. Comput. Sci. 612, 83–101 (2016)
  * [42] Solar-Lezama, A., Jones, C.G., Bodík, R.: Sketching concurrent data structures. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation. pp. 136–148. ACM (2008)
  * [43] Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: Shen, J.P., Martonosi, M. (eds.) Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006. pp. 404–415. ACM (2006)
  * [44] Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009. Lecture Notes in Computer Science, vol. 5584, pp. 244–257. Springer (2009)
  * [45] Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: Preliminary report. In: Aho, A.V., Borodin, A., Constable, R.L., Floyd, R.W., Harrison, M.A., Karp, R.M., Strong, H.R. (eds.) Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA. pp. 1–9. ACM (1973)
  * [46] Tentrup, L.: CAQE and quabs: Abstraction based QBF solvers. J. Satisf. Boolean Model. Comput. 11(1), 155–210 (2019)
  * [47] Tentrup, L., Rabe, M.N.: Clausal abstraction for DQBF. In: Janota, M., Lynce, I. (eds.) Theory and Applications of Satisfiability Testing - SAT 2019. Lecture Notes in Computer Science, vol. 11628, pp. 388–405. Springer (2019)
  * [48] Vizel, Y., Gurfinkel, A., Malik, S.: Fast interpolating BMC. In: Kroening, D., Pasareanu, C.S. (eds.) CAV 2015. Lecture Notes in Computer Science, vol. 9206, pp. 641–657. Springer (2015)
  * [49] Vizel, Y., Weissenbacher, G., Malik, S.: Boolean satisfiability solvers and their applications in model checking. Proc. IEEE 103(11), 2021–2035 (2015)
  * [50] Wimmer, R., Karrenbauer, A., Becker, R., Scholl, C., Becker, B.: From DQBF to QBF by dependency elimination. In: Gaspers, S., Walsh, T. (eds.) Theory and Applications of Satisfiability Testing - SAT 2017, Proceedings. Lecture Notes in Computer Science, vol. 10491, pp. 326–343. Springer (2017)
  * [51] Wimmer, R., Scholl, C., Becker, B.: The (D)QBF preprocessor hqspre - underlying theory and its implementation. J. Satisf. Boolean Model. Comput. 11(1), 3–52 (2019)
  * [52] Wimmer, R., Scholl, C., Wimmer, K., Becker, B.: Dependency schemes for DQBF. In: Creignou, N., Berre, D.L. (eds.) Theory and Applications of Satisfiability Testing - SAT 2016. Lecture Notes in Computer Science, vol. 9710, pp. 473–489. Springer (2016)