Fine-Grained Complexity Analysis of Dependency Quantified Boolean Formulas

Cheng, Che; Fung, Long-Hin; Jiang, Jie-Hong Roland; Slivovsky, Friedrich; Tan, Tony

doi:10.4230/LIPIcs.SAT.2025.10

Fine-Grained Complexity Analysis of Dependency Quantified Boolean Formulas

Che Cheng

Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan Long-Hin Fung

Department of Computer Science and Information Engineering, National Taiwan University, Taipei, Taiwan Jie-Hong Roland Jiang

Department of Electrical Engineering, National Taiwan University, Taipei, Taiwan Friedrich Slivovsky

Department of Computer Science, University of Liverpool, UK Tony Tan

Department of Computer Science, University of Liverpool, UK

Abstract

Dependency Quantified Boolean Formulas (DQBF) extend Quantified Boolean Formulas by allowing each existential variable to depend on an explicitly specified subset of the universal variables. The satisfiability problem for DQBF is NEXP-complete in general, with only a few tractable fragments known to date. We investigate the complexity of DQBF with $k$ existential variables ( $k$ -DQBF) under structural restrictions on the matrix – specifically, when it is in Conjunctive Normal Form (CNF) or Disjunctive Normal Form (DNF) – as well as under constraints on the dependency sets. For DNF matrices, we obtain a clear classification: $2$ -DQBF is PSPACE-complete, while $3$ -DQBF is NEXP-hard, even with disjoint dependencies. For CNF matrices, the picture is more nuanced: we show that the complexity of $k$ -DQBF ranges from NL-complete for $2$ -DQBF with disjoint dependencies to NEXP-complete for $6$ -DQBF with arbitrary dependencies.

Keywords and phrases:

Dependency quantified Boolean formulas, complexity, completeness, conjunctive normal form, disjunctive normal form

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Problems, reductions and completeness

Funding:

We would like to acknowledge the generous support of Royal Society International Exchange Grant no. EC\R3\233183, the National Science and Technology Council of Taiwan under grant NSTC 111-2923-E-002-013-MY3, and the NTU Center of Data Intelligence: Technologies, Applications, and Systems under grant NTU-113L900903.

DOI:

10.4230/LIPIcs.SAT.2025.10

Event:

28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Editors:

Jeremias Berg and Jakob Nordström

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Propositional satisfiability (SAT) solving has made significant progress over the past 30 years [4, 10]. Thanks to clever algorithms and highly optimised solvers, SAT has become a powerful tool for solving hard combinatorial problems in many areas, including verification, planning, and artificial intelligence [5]. Modern solvers can handle very large formulas efficiently, making SAT a practical choice in many settings.

However, for problems beyond NP, such as variants of reactive synthesis, direct encodings in propositional logic often grow exponentially with the input and quickly become too large to fit in memory. This has led to growing interest in more expressive logics, such as Quantified Boolean Formulas (QBF) and Dependency Quantified Boolean Formulas (DQBF) [17]. DQBF extends QBF by allowing explicit control over the dependency sets: each existential variable can be assigned its own set of universal variables it depends on. A model of a DQBF assigns to each existential variable a Skolem function that maps assignments of its dependency set to truth values. From a game-theoretic point of view, a DQBF model is a collection of sets of local strategies – one set for each existential variable – that may observe only part of the universal assignment. This makes DQBF more succinct than QBF and particularly well-suited for applications such as synthesis and verification, where components often make decisions based on partial information. Unfortunately, this added expressiveness comes at a cost: DQBF satisfiability is NEXP-complete, and only a few tractable fragments are known [7, 8, 6, 18, 15]. One notable tractable case involves CNF matrices with dependency sets that are either pairwise disjoint or identical; such formulas can be rewritten into satisfiability-equivalent $\Sigma_{3}$ -QBFs [18].

Building on these ideas, we apply similar restrictions on the dependency sets to refine a recent classification of the complexity of DQBF with $k$ existential variables ( $k$ -DQBF) [14]. For DNF matrices, this restriction has no effect, since the proofs in [14] for the PSPACE-hardness of $2$ -DQBF and NEXP-hardness of $3$ -DQBF can be carried over to formulas with pairwise disjoint dependency sets.

For CNF matrices, the situation is more subtle. For $k\geqslant 3$ and even non-constant $k$ with disjoint dependencies, we extend the strategy of [18] to split clauses containing variables with incomparable dependency sets, but instead of reducing it to a QBF, we directly construct an NP algorithm to establish the NP membership. This technique can be extended to the case where any two dependency sets are either disjoint or comparable, and the size blow-up remains polynomial for constant $k$ . The resulting DQBF only has existential variables with empty dependency sets, and its satisfiability can be checked in NP.

When arbitrary dependencies are allowed in CNF matrices, we prove that $3$ -DQBF is $\mathrm{\Pi_{2}^{P}}$ -hard. Further, a variant of Tseitin transformation lets us convert a $k$ -DQBF with an arbitrary matrix into a $(k+3)$ -DQBF with CNF matrix, yielding PSPACE-hardness of $5$ -DQBF and NEXP-hardness of $6$ -DQBF with CNF matrices.

As for the satisfiability problem of $2$ -DQBF, [13] shows that it reduces to detecting contradicting cycles in a succinctly represented implication graph, making it PSPACE-complete. For CNF matrices and disjoint dependencies, we show that the fully expanded graph has a simple structure, allowing satisfiability tests in NL. Consequently, the satisfiability of $2$ -DQBF with CNF matrices and unrestricted dependencies is in coNP – one can guess an assignment to the shared universal variables and solve the resulting instance with disjoint dependencies in NL. We also prove the NL- and coNP-hardness of the two problems via a reduction from $2$ -SAT and $3$ -DNF tautology, respectively.

Our results, summarised in Table 1, help map out the complexity of natural fragments of DQBF and show how both the formula structure and dependency restrictions play a key role in determining tractability.

Table 1: Summary of the complexity results.

k

k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}

k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{de}}}

k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{dec}}}

,

k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{ds}}}

k\textup{-DQBF}_{\textup{{cnf}}}

k\textup{-DQBF}_{\textup{{dnf}}}^{\textup{{d}}}

1

–

L

(Theorem 19)

coNP-c

(Theorem 4)

2

NL-c

NL-c

NL-c

coNP-c

PSPACE-c

3,4

NP-c

(Theorem 14)

NP-c

(Corollary 17)

NP-c

(Corollary 17)

\mathrm{\Pi_{2}^{P}}

-h

(Theorem 21)

NEXP-c

(Theorem 4)

5

PSPACE-h

(Theorem 23)

6+

NEXP-c

(Theorem 23)

Non-const.

\mathrm{\Sigma_{3}^{P}}

-c [18]

NEXP-c [18]

Note: “-c” denotes “-complete”, “-h” denotes “-hard”, and “non-const.” denotes “non-constant.”

2 Preliminaries

In this section, we define the notation used throughout this paper and recall the necessary technical background. All logarithms have base 2. For a positive integer $m$ , $[m]$ denotes the set of integers $\{1,\dots,m\}$ .

Boolean values True and False are denoted by $\top$ and $\bot$ , respectively. Boolean connectives $\wedge$ , $\vee$ , $\neg$ , $\rightarrow$ , $\leftrightarrow$ , and $\oplus$ are interpreted as usual. A literal $\ell$ is a Boolean variable $v$ or its negation $\neg v$ . We write $\operatorname{var}(v)=\operatorname{var}(\neg v)=v$ for the variable of a literal and $\operatorname{sgn}(v)=\top$ and $\operatorname{sgn}(\neg v)=\bot$ to denote its sign. We also write $v\oplus\bot$ and $v\oplus\top$ to denote the literals $v$ and $\neg v$ , respectively.

A clause is a disjunction of literals, and a cube is a conjunction of literals. A Boolean formula $\varphi$ is in conjunctive normal form (CNF) if it is a conjunction of clauses and in disjunctive normal form (DNF) if it is a disjunction of cubes. We view a clause or a cube as a set of literals and a formula in CNF (respectively, DNF) as a set of clauses (respectively, cubes) whenever appropriate. We sometimes write a clause in the form of $Q\rightarrow C$ , where $Q$ is a cube and $C$ is a clause, and similarly a DNF formula in the form of $\varphi\rightarrow\psi$ , where $\varphi$ is in CNF and $\psi$ is in DNF.

We say that two sets of clauses $A$ and $B$ are variable-disjoint if for any clause $C_{1}\in A$ and $C_{2}\in B$ , $C_{1}$ and $C_{2}$ do not share a common variable. For variable-disjoint sets $A$ and $B$ , we write $A\times B$ to denote the set of clauses $\{(C_{1}\vee C_{2})\nonscript\,|\allowbreak\nonscript\,\mathopen{}C_{1}\in A,C% _{2}\in B\}$ . We generalise this notion to $A_{1}\times A_{2}\times\cdots\times A_{n}$ for pairwise variable-disjoint sets $A_{1},\ldots,A_{n}$ .

We write $\bar{v}=(v_{1},\dots,v_{n})$ to denote a vector of $n$ Boolean variables with $\lvert\bar{v}\rvert\coloneqq n$ denoting its length.¹¹1To avoid clutter, we always assume a vector of variables $\bar{v}=(v_{1},\ldots,v_{n})$ do not contain duplicate entries, which can be viewed as a set $\{v_{1},\ldots,v_{n}\}$ . We will thus use set-theoretic operations on such vectors as on sets. An assignment on $\bar{v}$ is a function from $\bar{v}$ to $\{\top,\bot\}$ . We often identify an assignment on $\bar{v}$ with a vector $\bar{a}=(a_{1},\dots,a_{n})\in\{\top,\bot\}^{n}$ , denoted $\bar{a}^{\bar{v}}$ , which maps each $v_{i}$ to $a_{i}$ . When $\bar{v}\subseteq\bar{u}$ , we write $\bar{a}^{\bar{u}}(\bar{v})$ to denote the vector of Boolean values $(\bar{a}^{\bar{u}}(v))_{v\in\bar{v}}$ . When $\bar{v}$ is clear from the context, we will simply write $\bar{a}$ instead of $\bar{a}^{\bar{v}}$ .

Two assignments $\bar{a}^{\bar{u}}$ and $\bar{b}^{\bar{v}}$ are consistent, denoted by $\bar{a}^{\bar{u}}\simeq\bar{b}^{\bar{v}}$ , if $\bar{a}^{\bar{u}}(v)=\bar{b}^{\bar{v}}(v)$ for every $v\in\bar{u}\cap\bar{v}$ . When $\bar{a}^{\bar{u}}$ and $\bar{b}^{\bar{v}}$ are consistent, we write $(\bar{a}^{\bar{u}},\bar{b}^{\bar{v}})$ to denote the union $\bar{a}^{\bar{u}}\cup\bar{b}^{\bar{v}}$ . Given a Boolean formula $\phi$ over the variables $\bar{u},\bar{v}$ and an assignment $\bar{a}^{\bar{v}}$ , we denote by $\phi[\bar{a}^{\bar{v}}]$ the induced formula over the variables $\bar{u}$ obtained by assigning the variables in $\bar{v}$ with Boolean values according to the assignment $\bar{a}^{\bar{v}}$ .

For a positive integer $m$ and a vector of variables $\bar{u}$ of length $n>\log m$ , by abuse of notation, we write $\bar{u}=m$ to denote the cube $\bigwedge_{i\in[n]}u_{i}\leftrightarrow a_{i}$ , where $(a_{1},\ldots,a_{n})$ is the $n$ -bit binary representation of $m$ .

2.1 DQBF and Its Subclasses

We consider Dependency Quantified Boolean Formulas (DQBF) of the form

\addcontentsline{lla}{section}{\numberline{\string\crtrefnumber{eq:dqbf-% generic}}{e}q:dqbf-generic}\Phi=\forall\bar{x},\exists y_{1}(D_{1}),\dots,y_{k% }(D_{k}).\,\varphi\,,

(1)

where $\bar{x}=(x_{1},\dots,x_{n})$ , $D_{i}\subseteq\bar{x}$ is the dependency set of the existential variable $y_{i}$ for every $i\in[k]$ , and $\varphi$ is a quantifier-free Boolean formula over the variables $\bar{x}\cup\bar{y}$ called the matrix of $\Phi$ . We write $\operatorname{dep}(v)\coloneqq D_{i}$ if $v=y_{i}$ and $\operatorname{dep}(v)\coloneqq\{x_{i}\}$ if $v=x_{i}$ . We extend this notation to literals and clauses by letting $\operatorname{dep}(\ell)\coloneqq\operatorname{dep}(\operatorname{var}(\ell))$ for a literal $\ell$ and $\operatorname{dep}(C)\coloneqq\bigcup_{\ell\in C}\operatorname{dep}(\ell)$ for a clause $C$ .

We say that $\Phi$ is satisfiable if for every $i\in[k]$ there is a Boolean formula $f_{i}$ using only variables in $D_{i}$ such that by replacing each $y_{i}$ with $f_{i}$ , the formula $\varphi$ becomes a tautology. In this case, we call the sequence $f_{1},\dots,f_{k}$ a model of $\Phi$ and refer to each individual $f_{i}$ as a Skolem function for $y_{i}$ .

We define the subclasses $k\textup{-DQBF}_{\textup{{$\beta$}}}^{\textup{{$\alpha$}}}$ of DQBF, where $k\geqslant 1$ indicates the number of existential variables, $\alpha\in\{\textup{{d}},\textup{{de}},\textup{{dec}},\textup{{ds}}\}$ indicates the condition on the dependency sets, and $\beta\in\{\textup{{cnf}},\textup{{dnf}}\}$ indicates the form of the matrix.

For the dependency set annotation $\alpha$ , we define:

$\textup{DQBF}^{\textup{{d}}}$: For every $i\neq j$ , $D_{i}\cap D_{j}=\emptyset$ ,
$\textup{DQBF}^{\textup{{de}}}$: For every $i\neq j$ , $D_{i}\cap D_{j}=\emptyset$ or $D_{i}=D_{j}$ ,
$\textup{DQBF}^{\textup{{dec}}}$: For every $i\neq j$ with $\lvert D_{i}\rvert\leqslant\lvert D_{j}\rvert$ , $D_{i}\cap D_{j}=\emptyset$ , $D_{i}=D_{j}$ , or $D_{j}=\bar{x}$ , and
$\textup{DQBF}^{\textup{{ds}}}$: For every $i\neq j$ with $\lvert D_{i}\rvert\leqslant\lvert D_{j}\rvert$ , $D_{i}\cap D_{j}=\emptyset$ or $D_{i}\subseteq D_{j}$ .

The letters d, e, c, and s denote disjoint, equal, complete, and subset, respectively. Note that the dependency sets of a $\textup{DQBF}^{\textup{{ds}}}$ formula form a laminar set family. The classification of different dependency structures is inspired by [18], but we specify the condition that the formula is in CNF explicitly in our notation. That is, DQBF^de and DQBF^dec in [18] correspond to $\textup{DQBF}_{\textup{{cnf}}}^{\textup{{de}}}$ and $\textup{DQBF}_{\textup{{cnf}}}^{\textup{{dec}}}$ in our notation, respectively.

Note that $\textup{DQBF}^{\textup{{d}}}\subseteq\textup{DQBF}^{\textup{{de}}}\subseteq% \textup{DQBF}^{\textup{{dec}}}\subseteq\textup{DQBF}^{\textup{{ds}}}$ . The first two inclusions are trivial, and the last one comes from the observation that both $D_{i}=D_{j}$ and $D_{j}=\bar{x}$ are special cases of $D_{i}\subseteq D_{j}$ .

When $k$ , $\alpha$ , or $\beta$ is missing, it means that the corresponding restriction is dropped. For instance, $3\textup{-DQBF}_{\textup{{dnf}}}$ denotes the class of DQBF with $3$ existential variables, arbitrary dependency structure, and matrix in DNF, while $\textup{DQBF}^{\textup{{d}}}$ denotes the class of DQBF with the dependency structure specified by d and an arbitrary Boolean formula as the matrix. We denote by $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{$\beta$}}}^{\textup{{$% \alpha$}}})$ the satisfiability problem for the class $k\textup{-DQBF}_{\textup{{$\beta$}}}^{\textup{{$\alpha$}}}$ .

$\blacktriangleright$ Remark 1.

For every $\alpha\in\{\textup{{d}},\textup{{de}},\textup{{dec}},\textup{{ds}}\}$ and $\beta\in\{\textup{{cnf}},\textup{{dnf}}\}$ , checking whether a DQBF formula $\Phi$ is in the class $\textup{DQBF}_{\textup{{$\beta$}}}^{\textup{{$\alpha$}}}$ can be done deterministically in space logarithmic in the length of $\Phi$ . To do so, we iterate through all the variables to check whether it satisfies the conditions set by $\alpha$ . In each iteration, it suffices to store $O(1)$ number of indices of the variables, which requires only logarithmic space.

2.2 Manipulation of $\textup{DQBF}_{\textup{{cnf}}}$

We recall two operations for manipulating $\textup{DQBF}_{\textup{{cnf}}}$ formulas, namely universal reduction [3, 12] and resolution-based variable elimination [20].

Lemma 2 (Universal reduction [3, 12]).

Let $\Phi=\forall\bar{x},\exists y_{1}(D_{1}),\dots,\exists y_{k}(D_{k}).\,\varphi$ be a $\textup{DQBF}_{\textup{{cnf}}}$ formula, $C\in\varphi$ be a clause, $\ell\in C$ be a universal literal, and let $C^{\prime}\coloneqq C\setminus\{\ell\}$ . If $\ell\notin\operatorname{dep}(C^{\prime})$ , then $\Phi$ is equisatisfiable to

\Phi^{\prime}\coloneqq\forall\bar{x},\exists y_{1}(D_{1}),\dots,\exists y_{k}(% D_{k}).\,\varphi\cup\{C^{\prime}\}\setminus\{C\}\,.

Using universal reduction, we assume that $\bigcup_{i\in[k]}D_{i}=\bar{x}$ for every $\textup{DQBF}_{\textup{{cnf}}}$ formula, since any universal variable not in $\bigcup_{i\in[k]}D_{i}$ can be universally-reduced from every clause.

For variable elimination by resolution, we only need a weaker version, which is sufficient for our purpose.

Lemma 3 (Variable elimination by resolution [20]).

Let $\Phi=\forall\bar{x},\exists y_{1}(D_{1}),\dots,\exists y_{k}(D_{k}).\,\varphi$ be a $\textup{DQBF}_{\textup{{cnf}}}$ formula. We partition $\varphi$ into three sets:

$\blacksquare$

$\varphi^{y_{1}}\coloneqq\{C\in\varphi\nonscript\,|\allowbreak\nonscript\,% \mathopen{}y_{1}\in C\}$ ,
$\blacksquare$

$\varphi^{\neg y_{1}}\coloneqq\{C\in\varphi\nonscript\,|\allowbreak\nonscript\,% \mathopen{}\neg y_{1}\in C\}$ , and
$\blacksquare$

$\varphi^{\emptyset}\coloneqq\varphi\setminus(\varphi^{y_{1}}\cup\varphi^{\neg y% _{1}})$ .

If for every $C\in\varphi^{y_{1}}$ we have $\operatorname{dep}(C)\subseteq\operatorname{dep}(y_{1})$ , or for every $C\in\varphi^{\neg y_{1}}$ we have $\operatorname{dep}(C)\subseteq\operatorname{dep}(y_{1})$ , then $\Phi$ is equisatisfiable to

\forall\bar{x},\exists y_{2}(D_{2}),\dots,\exists y_{k}(D_{k}).\,\varphi^{% \emptyset}\cup\{C\otimes_{y_{1}}C^{\prime}\nonscript\,|\allowbreak\nonscript\,% \mathopen{}C\in\varphi^{y_{1}},C^{\prime}\in\varphi^{\neg y_{1}}\}\,,

where $C\otimes_{v}C^{\prime}$ denotes the resolution of $C$ and $C^{\prime}$ w.r.t. the pivot $v$ , i.e., $C\otimes_{v}C^{\prime}=(C\setminus\{v\})\cup(C^{\prime}\setminus\{\neg v\})$ .

The intuition is that $y_{1}$ can “see” every assignment that may force it to be assigned to $\top$ (respectively, $\bot$ ), and thus if all resolvents are satisfied, then there must be a Skolem function for $y_{1}$ that satisfies the clauses in $\varphi^{y_{1}}\cup\varphi^{\neg y_{1}}$ . Note that the number of clauses after removing $y_{1}$ is at most $\lvert\varphi\rvert^{2}$ .

2.3 Universal Expansion of $k\textup{-DQBF}$

Consider a $k\textup{-DQBF}$ formula $\Phi\coloneqq\forall\bar{x},\exists y_{1}(D_{1}),\dots,\exists y_{k}(D_{k}).\,\varphi$ . Let $\bar{y}=(y_{1},\dots,y_{k})$ . Given an assignment $\bar{a}$ on $\bar{x}$ and $\bar{b}$ on $\bar{y}$ , for every $i\in[k]$ , let $\bar{a}_{i}$ be the restriction of $\bar{a}$ to $D_{i}$ and $b_{i}$ be the restriction of $\bar{b}$ to $y_{i}$ . We can expand $\Phi$ into an equisatisfiable $k$ -CNF formula $\exp(\Phi)$ by instantiating each $y_{i}$ into exponentially many instantiated variables of the form $Y_{i,\bar{a}_{i}}$ [2, 6, 12]. Formally,

\exp(\Phi)\coloneqq\bigwedge_{(\bar{a},\bar{b}):\varphi[\bar{a},\bar{b}]=\bot}% \mathcal{C}_{\bar{a},\bar{b}}\,,

where $\mathcal{C}_{\bar{a},\bar{b}}\coloneqq\bigvee_{i\in[k]}Y_{i,\bar{a}_{i}}\oplus b% _{i}$ . Intuitively, in the expansion $\exp(\Phi)$ , the Boolean variable $Y_{i,\bar{a}_{i}}$ represents the value of a candidate Skolem function $f_{i}(\bar{a}_{i})$ for $y_{i}$ . The universal expansion shows that the satisfiability of $\Phi$ can be reduced to a Boolean satisfiability problem (with exponential blow-up). Moreover, if the assignment $(\bar{a},\bar{b})$ falsifies the matrix $\varphi$ , then a satisfying assignment of $\exp(\Phi)$ must assign $Y_{i,\bar{a}_{i}}$ to $\neg b_{i}$ for some $i\in[k]$ .

3 Complexity of $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{dnf}}}^{\textup{{d}}})$

Having defined the various subclasses of DQBF, we can refine previous results by stating them more precisely. In this section, we consider the case where the matrix is in DNF.

By combining the DNF version of Tseitin transformation [9, Proposition 1] and the results in [14], we can show that restricting to DNF matrix and pairwise-disjoint dependency sets does not affect the complexity of $\operatorname{\textup{{sat}}}(k\textup{-DQBF})$ .

Theorem 4.

$\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{dnf}}}^{\textup{{d}}})$ is coNP-, PSPACE-, and NEXP-complete when $k=1$ , $k=2$ , and $k\geqslant 3$ , respectively.

See the appendix for the detailed proof. Since $k\textup{-DQBF}_{\textup{{dnf}}}^{\textup{{d}}}\subseteq k\textup{-DQBF}_{% \textup{{dnf}}}^{\textup{{de}}}\subseteq k\textup{-DQBF}_{\textup{{dnf}}}^{% \textup{{dec}}}\subseteq k\textup{-DQBF}_{\textup{{dnf}}}^{\textup{{ds}}}% \subseteq k\textup{-DQBF}_{\textup{{dnf}}}\subseteq k\textup{-DQBF}$ , we have the following corollary:

Corollary 5.

$\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{dnf}}}^{\textup{{$% \alpha$}}})$ and $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{dnf}}})$ is coNP-, PSPACE-, and NEXP-complete when $k=1$ , $k=2$ , and $k\geqslant 3$ , respectively, for every $\alpha\in\{\textup{{de}},\textup{{dec}},\textup{{ds}}\}$ .

4 Complexity of $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{$% \alpha$}}})$

In this section, we consider the complexity of $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{$% \alpha$}}})$ and $\operatorname{\textup{{sat}}}(\textup{DQBF}_{\textup{{cnf}}}^{\textup{{$\alpha% $}}})$ , with a focus on the case where $\alpha=\textup{{d}}$ . We first prove an important property of the expansion of $\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ formulas in Section 4.1 Then, in Sections 4.2 and 4.3 we show that $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ is of the same complexity as $k$ -SAT for $k\geqslant 2$ ,²²2There is no dependency structure for $k=1$ . and that $\operatorname{\textup{{sat}}}(\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ is of the same complexity as SAT. This shows that, in stark contrast to the DNF case in the previous section, with pairwise disjoint dependency sets and with CNF matrix, the exponential gap between SAT and DQBF disappears. Finally, we discuss other dependency structures in Section 4.4.

4.1 Universal Expansion of $\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$

In this section, we show a useful property of the expansion of $\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ formulas. We fix a $k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ formula:

\displaystyle\addcontentsline{lla}{section}{\numberline{\string\crtrefnumber{% eq:notation-d-dqbf}}{e}q:notation-d-dqbf}\Phi=\forall\bar{x},\exists y_{1}(D_{% 1}),\dots,\exists y_{k}(D_{k}).\,\bigwedge_{j\in[m]}C_{j}.

(2)

Let $\bar{y}=(y_{1},\dots,y_{k})$ . Given an assignment $\bar{a}$ on $\bar{x}$ and $\bar{b}$ on $\bar{y}$ , for every $i\in[k]$ , let $\bar{a}_{i}$ be the restriction of $\bar{a}$ to $D_{i}$ and $b_{i}$ be the restriction of $\bar{b}$ to $y_{i}$ .

Recall that for a DQBF formula $\Phi$ , each instantiated clause in $\exp(\Phi)$ corresponds to a falsifying assignment of the matrix of $\Phi$ . For a formula in CNF, the set of falsifying assignments can be represented by the union of the set of falsifying assignments of each individual clause. This allows us to represent the instantiated clauses in $\exp(\Phi)$ as the union of polynomially many sets when $\Phi$ is a $\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ formula. Moreover, the disjoint dependency structure allows us to further represent each of these sets as the Cartesian product of variable-disjoint sets of instantiated literals. To formally state the property, we first define some notation.

For a clause $C_{j}$ in $\Phi$ , we write $C_{j}^{i}(\Phi)$ to denote the subset of $C_{j}$ within $y_{i}$ ’s dependency set, $\mathcal{L}_{i,j}(\Phi)$ the set of instantiated literals $Y_{i,\bar{a}_{i}}\oplus b_{i}$ where the assignment $(\bar{a}_{i},b_{i})$ falsifies $C_{j}^{i}$ , and $\mathfrak{C}_{j}(\Phi)$ the set of instantiated clauses $\mathcal{C}_{\bar{a},\bar{b}}$ where $(\bar{a},\bar{b})$ falsifies $\neg C_{j}$ . We now formally define these sets.

Definition 6.

Let $\Phi$ be a $k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ formula as in (2). For every $j\in[m]$ and $i\in[k]$ , we define the sets $C_{j}^{i}(\Phi)$ , $\mathcal{L}_{i,j}(\Phi)$ and $\mathfrak{C}_{j}(\Phi)$ :

$\blacksquare$

$C_{j}^{i}(\Phi)\coloneqq\{\ell\in C_{j}\nonscript\,|\allowbreak\nonscript\,% \mathopen{}\operatorname{var}(\ell)\in D_{i}\cup\{y_{i}\}\}$ .
$\blacksquare$

$\mathcal{L}_{i,j}(\Phi)\coloneqq\{Y_{i,\bar{a}_{i}}\oplus b_{i}\nonscript\,|% \allowbreak\nonscript\,\mathopen{}(\bar{a}_{i},b_{i})\simeq\neg C_{j}^{i}\}$ .
$\blacksquare$

$\mathfrak{C}_{j}(\Phi)\coloneqq\left\{\mathcal{C}_{\bar{a},\bar{b}}\nonscript% \,\middle|\allowbreak\nonscript\,\mathopen{}(\bar{a},\bar{b})\simeq\neg C_{j}\right\}$ .

When $\Phi$ is clear from the context, we simply write $C_{j}^{i}$ , $\mathcal{L}_{i,j}$ and $\mathfrak{C}_{j}$ .

We remark that $(\bar{a},\bar{b})\simeq\neg C_{j}$ if and only if $(\bar{a},\bar{b})$ falsifies $C_{j}$ , and similarly $(\bar{a}_{i},b_{i})\simeq\neg C_{j}^{i}$ if and only if $(\bar{a}_{i},b_{i})$ falsifies $C_{j}^{i}$ . Note also that $\exp(\Phi)=\bigwedge_{j\in[m]}\bigwedge_{C\in\mathfrak{C}_{j}}C$ and that the sets $\mathcal{L}_{1,j},\ldots,\mathcal{L}_{k,j}$ are pairwise variable-disjoint.

We now state the property formally.

Lemma 7.

Let $\Phi$ be as in Equation 2. For every $j\in[m]$ , $\mathfrak{C}_{j}=\mathcal{L}_{1,j}\times\cdots\times\mathcal{L}_{k,j}$ .

Proof.

We fix an arbitrary $j\in[m]$ . We first prove the “ $\subseteq$ ” direction. Let $\mathcal{C}_{\bar{a},\bar{b}}$ be a clause in $\mathfrak{C}_{j}$ . That is, $(\bar{a},\bar{b})$ is an assignment that falsifies $C_{j}$ . Let $\bar{a}_{i}$ be the restriction of $\bar{a}$ on $D_{i}$ and $b_{i}$ be the restriction of $\bar{b}$ on $y_{i}$ , for every $i\in[k]$ . By definition, $\mathcal{C}_{\bar{a},\bar{b}}=\bigvee_{i\in[k]}Y_{i,\bar{a}_{i}}\oplus b_{i}$ . Since $(\bar{a},\bar{b})$ falsifies $C_{j}$ , it is consistent with the cube $\neg C_{j}$ . Hence, for every $i\in[k]$ , each $\bar{a}_{i},b_{i}$ is consistent with the cube $\neg C_{j}^{i}$ . By definition, the literal $Y_{i,\bar{a}_{i}}\oplus b_{i}$ belongs to $\mathcal{L}_{i,j}$ , for every $i\in[k]$ .

Next, we prove the “ $\supseteq$ ” direction. Let $C\coloneqq(L_{1}\vee\dots\vee L_{k})\in\mathcal{L}_{1,j}\times\cdots\times% \mathcal{L}_{k,j}$ . By definition, for every $i\in[k]$ , there is assignment $(\bar{a}_{i},b_{i})$ such that $L_{i}$ is the literal $Y_{i,\bar{a}_{i}}\oplus b_{i}$ and $(\bar{a}_{i},b_{i})$ is consistent with the cube $\neg C_{j}^{i}$ . Due to the disjointness of the dependency sets, all the assignments $(\bar{a}_{i},b_{i})$ ’s are pairwise consistent. Let $(\bar{a},\bar{b})$ be their union $\bigcup_{i\in[k]}(\bar{a}_{i},b_{i})$ .³³3Note that, as stated in Section 2.2, we assume that $\bigcup_{i\in[k]}D_{i}=\bar{x}$ . Since each $(\bar{a}_{i},b_{i})$ is consistent with $\neg C_{j}^{i}$ , $(\bar{a},\bar{b})$ is consistent with all of $\neg C_{j}^{1},\ldots,\neg C_{j}^{k}$ . Therefore, $(\bar{a},\bar{b})$ is a falsifying assignment of $C_{j}$ . By definition, the clause $\mathcal{C}_{\bar{a},\bar{b}}=\bigvee_{i\in[k]}Y_{i,\bar{a}_{i}}\oplus b_{i}$ is in $\mathfrak{C}_{j}$ . $\hfill\blacktriangleleft$

4.2 $2\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$

In this section we will show that $\operatorname{\textup{{sat}}}(2\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ is NL-complete, as stated formally in Theorem 8.

Theorem 8.

$\operatorname{\textup{{sat}}}(2\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ is NL-complete.

Before we proceed to the formal proof, we first review some notation and terminology. Recall that the expansion of a $2$ -DQBF formula (even when the matrix is in an arbitrary form) is a $2$ -CNF formula, which can be viewed as a directed graph, called the implication graph (of the $2$ -CNF formula) [1]. The vertices in the implication graph are the literals, and for every clause $(\ell\vee\ell^{\prime})$ in the formula, there are two edges, $(\neg\ell\to\ell^{\prime})$ and $(\neg\ell^{\prime}\to\ell)$ .

The following notion of a disimplex will be useful.

Definition 9 (Disimplex [11]).

Given two sets of vertices $\mathcal{A},\mathcal{B}$ , the disimplex from $\mathcal{A}$ to $\mathcal{B}$ is the directed graph $K(\mathcal{A},\mathcal{B})\coloneqq(\mathcal{A}\cup\mathcal{B},\mathcal{A}% \times\mathcal{B})$ .

In other words, a disimplex $K(\mathcal{A},\mathcal{B})$ is a complete directed bipartite graph where all the edges are oriented from $\mathcal{A}$ to $\mathcal{B}$ .

The rest of this subsection is devoted to the proof of Theorem 8. For the rest of this subsection, we fix a $2\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ formula $\Phi=\forall\bar{z}_{1},\bar{z}_{2},\exists y_{1}(\bar{z}_{1}),\exists y_{2}(% \bar{z}_{2}).\,\bigwedge_{j\in[m]}C_{j}$ . We will simply write $C_{j}^{i}$ , $\mathcal{L}_{i,j}$ and $\mathfrak{C}_{j}$ to denote the sets $C_{j}^{i}(\Phi)$ , $\mathcal{L}_{i,j}(\Phi)$ and $\mathfrak{C}_{j}(\Phi)$ defined in Definition 6. For a set $\mathcal{L}$ of literals, we denote by $\widehat{\mathcal{L}}$ the set of negated literals in $\mathcal{L}$ , i.e., $\widehat{\mathcal{L}}\coloneqq\{\neg L\nonscript\,|\allowbreak\nonscript\,% \mathopen{}L\in\mathcal{L}\}$ .

We first show that the implication graph of $\exp(\Phi)$ is a finite union of disimplices, and that the length of any shortest path between two vertices is bounded above by $2m$ .

Lemma 10.

Let $G=(\mathcal{V},\mathcal{E})$ be the implication graph of $\exp(\Phi)$ . The set of edges $\mathcal{E}$ can be represented as

\mathcal{E}=\bigcup_{j\in[m]}(\widehat{\mathcal{L}}_{1,j}\times\mathcal{L}_{2,% j})\cup(\widehat{\mathcal{L}}_{2,j}\times\mathcal{L}_{1,j})\,,

which is the union of the edge sets of $m$ pairs of disimplices. Moreover, for every two vertices $L,L^{\prime}\in\mathcal{V}$ , if $L^{\prime}$ is reachable from $L$ , then there exists a path from $L$ to $L^{\prime}$ of length at most $2m$ .

Proof.

By definition,

\mathcal{E}=\left\{(\neg Y_{1,\bar{z}_{1}}\oplus b_{1},Y_{2,\bar{z}_{2}}\oplus b% _{2}),(\neg Y_{2,\bar{z}_{2}}\oplus b_{2},Y_{1,\bar{z}_{1}}\oplus b_{1})% \nonscript\,\middle|\allowbreak\nonscript\,\mathopen{}\varphi[\bar{a}_{1}^{% \bar{z}_{1}},\bar{a}_{2}^{\bar{z}_{2}},b_{1}^{y_{1}},b_{2}^{y_{2}}]=\bot\right% \}\,.

Since any assignment that falsifies $\varphi$ must falsify some clause $C_{j}$ in $\varphi$ , we have

\mathcal{E}=\bigcup_{j\in[m]}\bigcup_{\mathcal{C}_{\bar{a},\bar{b}}\in% \mathfrak{C}_{j}}\left\{(\neg Y_{1,\bar{z}_{1}}\oplus b_{1},Y_{2,\bar{z}_{2}}% \oplus b_{2}),(\neg Y_{2,\bar{z}_{2}}\oplus b_{2},Y_{1,\bar{z}_{1}}\oplus b_{1% })\right\}\,.

By Lemma 7, we have $\mathfrak{C}_{j}=\{(L_{1}\vee L_{2})\nonscript\,|\allowbreak\nonscript\,% \mathopen{}L_{1}\in\mathcal{L}_{1,j},L_{2}\in\mathcal{L}_{2,j}\}$ for every $j\in[m]$ . Therefore,

\mathcal{E}=\bigcup_{j\in[m]}\left(\widehat{\mathcal{L}}_{1,j}\times\mathcal{L% }_{2,j}\right)\cup\left(\widehat{\mathcal{L}}_{2,j}\times\mathcal{L}_{1,j}% \right)\,.

For the second part of the proof, assume, for the sake of contradiction, that $P=(L_{0},\dots,L_{n})$ is a shortest path from $L$ to $L^{\prime}$ with $n>2m$ . Then, by the pigeonhole principle, there must be some $0\leqslant i_{1}<i_{2}<n$ such that $(L_{i_{1}},L_{i_{1}+1})$ and $(L_{i_{2}},L_{i_{2}+1})$ belongs to the same disimplex $K\subseteq\mathcal{E}$ , and thus $(L_{i_{1}},L_{i_{2}+1})\in K\subseteq\mathcal{E}$ . We can then construct a shorter path $P^{\prime}=(L_{0},\dots,L_{i_{1}},L_{i_{2}+1},\dots,L_{n})$ from $L$ to $L^{\prime}$ , which contradicts with the assumption that $P$ is a shortest path. $\hfill\blacktriangleleft$

Proof of Theorem 8.

For the NL membership, we devise an algorithm by checking the unsatisfiability of $\exp(\Phi)$ directly on these disimplices. We present an NL algorithm that checks the unsatisfiability of $\exp(\Phi)$ by looking for cycles containing both an instantiated literal and its negation in the implication graph $G=(\mathcal{V},\mathcal{E})$ of $\exp(\Phi)$ .⁴⁴4Recall that a $2$ -SAT formula $\varphi$ is unsatisfiable if and only if there is a cycle containing both a literal and its negation in the implication graph of $\varphi$ .

A naïve idea is to first non-deterministically guess a literal $L$ and the paths $P$ from $L$ to $\neg L$ and $P^{\prime}$ from $\neg L$ to $L$ . However, since $\lvert\mathcal{V}\rvert$ is exponential in $\lvert\bar{x}\rvert$ , representing a literal $L\in\mathcal{V}$ takes linear space. We instead make use of Lemma 10 and guess the disimplex each edge of $P,P^{\prime}$ belongs in, denoted by the sequences $(K(\mathcal{A}_{1},\mathcal{B}_{1}),\dots,K(\mathcal{A}_{n},\mathcal{B}_{n}))$ and $(K(\mathcal{A}_{1}^{\prime},\mathcal{B}_{1}^{\prime}),\dots,K(\mathcal{A}_{n^{% \prime}}^{\prime},\mathcal{B}_{n^{\prime}}^{\prime}))$ with $n,n^{\prime}\in[2m]$ , where each $\mathcal{A},\mathcal{B}$ is of the form $\mathcal{L}_{i,j}$ or $\widehat{\mathcal{L}}_{i,j}$ . We then check if

$\blacksquare$

for every step $j\in[n-1]$ , whether there exists some $L_{j}\in\mathcal{B}_{j}\cap\mathcal{A}_{j+1}$ ,
$\blacksquare$

for every step $j^{\prime}\in[n^{\prime}-1]$ , whether there exists some $L^{\prime}_{j^{\prime}}\in\mathcal{B}_{j^{\prime}}^{\prime}\cap\mathcal{A}_{j^% {\prime}+1}^{\prime}$ , and
$\blacksquare$

whether there exists some $L_{0}\in\mathcal{A}_{1}\cap\widehat{\mathcal{B}}_{n}\cap\widehat{\mathcal{A}}_% {1}^{\prime}\cap\mathcal{B}_{n^{\prime}}^{\prime}$ .

We reject if one of the checks fails, and accept if all checks succeed. In the latter case, there are paths $P=(L_{0},L_{1},\dots,L_{n-1},\neg L_{0})$ and $P^{\prime}=(\neg L_{0},L_{1}^{\prime},L_{2}^{\prime},\dots,L_{n^{\prime}-1}^{% \prime},L_{0})$ .

In particular, $\mathcal{L}_{i,j}\cap\mathcal{L}_{i^{\prime},j^{\prime}}$ is non-empty if and only if $i=i^{\prime}$ and $C_{j}^{i}$ and $C_{j^{\prime}}^{i^{\prime}}$ are consistent. The consistency check can be done by keeping two pointers to the position in the clause using $\log(\lvert\bar{x}\rvert+2)$ bits per pointer. This can easily be generalised to check the intersection of any constant number of $\mathcal{L}_{i,j}$ ’s. For $\widehat{\mathcal{L}}_{i,j}$ , simply replace $C_{j}^{i}$ with the clause $\hat{C}_{j}^{i}$ with the sign of $y_{i}$ flipped if a literal of $y_{i}$ is present, i.e.,

\hat{C}_{j}^{i}\coloneqq\left(C_{j}^{i}\setminus\{y_{i},\neg y_{i}\}\right)% \cup\left(\neg C_{j}^{i}\cap\{y_{i},\neg y_{i}\}\right)\,.

For the hardness proof, we provide a reduction from $2$ -SAT to $2\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ . Let $\varphi=\bigwedge_{j\in[m]}(\ell_{j,1}\vee\ell_{j,2})$ be a $2$ -CNF formula over the variables $\bar{x}=(x_{1},\dots,x_{n})$ . The idea is to encode the assignment of $\bar{x}$ with a function $f:[n]\to\{\bot,\top\}$ where $f(i)$ represents the assignment of $x_{i}$ .

In the following, for a literal $\ell$ , let $\operatorname{ind}(\ell)$ denote the index $i$ where $x_{i}=\operatorname{var}(\ell)$ . We construct the $2\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ formula

\Psi\coloneqq\forall\bar{u}_{1},\forall\bar{u}_{2},\exists y_{1}(\bar{u}_{1}),% \exists y_{2}(\bar{u}_{2}).\,\psi\,,

where $\bar{u}_{1}$ and $\bar{u}_{2}$ have length $O(\log n)$ for representing the variables in $\bar{x}$ and $\psi$ is a CNF formula that states the following.

$\blacksquare$

$((\bar{u}_{1}=i)\land(\bar{u}_{2}=i))\to(y_{1}\leftrightarrow y_{2})$ for every $i\in[n]$ .
$\blacksquare$

$((\bar{u}_{1}=\operatorname{ind}(\ell_{j,1}))\land(\bar{u}_{2}=\operatorname{% ind}(\ell_{j,2})))\to((y_{1}\leftrightarrow\operatorname{sgn}(\ell_{j,1}))\lor% (y_{2}\leftrightarrow\operatorname{sgn}(\ell_{j,2})))$ for every $j\in[m]$ .

The first item states that the Skolem functions for $y_{1}$ and $y_{2}$ must be the same. The second item implies that $\bar{a}^{\bar{x}}$ is a satisfying assignment of $\varphi$ if and only if the function $f_{\bar{a}}$ is a Skolem function for $\Psi$ by encoding the assignment $\bar{a}^{\bar{x}}$ as a function $f_{\bar{a}}\colon[n]\to\{\top,\bot\}$ , where $f_{\bar{a}}(i)=\bar{a}^{\bar{x}}(x_{i})$ . $\hfill\blacktriangleleft$

4.3 $k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ : $k\geqslant 3$ and Non-Constant $𝒌$

For $k\geqslant 3$ and even arbitrary $\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ , we show that it is NP-complete. Let $\Phi$ be as in Equation 2. To show the NP membership, we first show that for every $j\in[m]$ , some $y_{i}$ is responsible for satisfying all the clauses in $\mathfrak{C}_{j}$ .

Lemma 11.

Let $\Phi$ be as in Equation 2 and let $\bar{Y}$ be the vector of variables in $\exp(\Phi)$ . For every $j\in[m]$ and every assignment $\bar{a}$ on $\bar{Y}$ , $\bar{a}$ satisfies the CNF formula $\bigwedge_{\mathcal{C}\in\mathfrak{C}_{j}}\mathcal{C}$ if and only if $\bar{a}$ satisfies the cube $\bigwedge_{L\in\mathcal{L}_{i,j}}L$ for some $i\in[k]$ .

Proof.

We first prove the “if” direction. Let $\bar{a}$ be an assignment on $\bar{Y}$ . If $\bar{a}$ satisfies the cube $\bigwedge_{L\in\mathcal{L}_{i,j}}L$ , then, for every clause $\mathcal{C}\in\mathfrak{C_{j}}$ , by Lemma 7, there exists some $L\in\mathcal{L}_{i,j}\cap\mathcal{C}$ that is satisfied by $\bar{a}$ . Thus, $\mathcal{C}$ is satisfied by $L$ .

For the “only if” direction, assume that $\bar{a}$ does not satisfy the cube $\bigwedge_{L\in\mathcal{L}_{i,j}}L$ for every $i\in[k]$ . That is, for every $i\in[k]$ , there exists some $L_{i}\in\mathcal{L}_{i,j}$ such that $\bar{a}(\operatorname{var}(L_{i}))\neq\operatorname{sgn}(L_{i})$ . It follows that the clause $\left(\bigvee_{i\in[k]}L_{i}\right)\in\mathfrak{C}_{j}$ is falsified by $\bar{a}$ , and thus $\bar{a}$ does not satisfy $\bigwedge_{\mathcal{C}\in\mathfrak{C}_{j}}\mathcal{C}$ . $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 12.

Recall that $\exp(\Phi)=\bigwedge_{j\in[m]}\bigwedge_{\mathcal{C}\in\mathfrak{C}_{j}}% \mathcal{C}$ . Thus, Lemma 11 can be reformulated as follows. For every assignment $\bar{a}^{\bar{Y}}$ , $\bar{a}^{\bar{Y}}$ satisfies $\exp(\Phi)$ if and only if there is a function $\xi:[m]\to[k]$ such that for every $j\in[m]$ , $\bar{a}^{\bar{Y}}$ satisfies the cube $\bigwedge_{L\in\mathcal{L}_{\xi(j),j}}L$ . Intuitively, the function $\xi$ is the mapping that maps index $j$ to index $i$ in the statement in Lemma 11. This formulation will be useful later on.

The next lemma shows the NP membership of $\operatorname{\textup{{sat}}}(\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ .

Lemma 13.

$\operatorname{\textup{{sat}}}(\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ is in NP.

Proof.

Consider a $\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ formula:

\Phi=\forall\bar{z}_{1},\dots,\forall\bar{z}_{k},\exists y_{1}(\bar{z}_{1}),% \dots,\exists y_{k}(\bar{z}_{k}).\,\bigwedge_{j\in[m]}C_{j}

with $k$ existential variables and $m$ clauses.

By the reformulation of Lemma 11 in Remark 12, an assignment $\bar{a}$ on $\bar{Y}$ satisfies $\exp(\Phi)$ if and only if there exists a mapping $\xi\colon[m]\to[k]$ such that $\bar{a}^{\bar{Y}}$ satisfies $\bigwedge_{j\in[m]}\bigwedge_{L\in\mathcal{L}_{\xi(j),j}}L$ , or equivalently, if there exists a partition $\{S_{i}\}_{i\in[k]}$ of $[m]$ such that for each $i\in[k]$ , the following QBF $\Phi_{i}$ is satisfiable:

\Phi_{i}=\forall\bar{z}_{i},\exists y_{i}.\,\bigwedge_{j\in S_{i}}C_{j}^{i}\,.

Note that since $\Phi_{i}$ contains only one existential variable and it depends on all universal variables, checking the satisfiability of $\Phi_{i}$ is in P using Lemma 3.⁵⁵5In fact, it is in L, as shown later in Theorem 19. An NP algorithm guesses the partition $\{S_{i}\}_{i\in[k]}$ and verifies that $\Phi_{i}$ is satisfiable for every $i\in[k]$ . $\hfill\blacktriangleleft$

Theorem 14.

$\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ for every $k\geqslant 3$ and $\operatorname{\textup{{sat}}}(\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ are NP-complete.

Proof.

By Lemma 13, $\operatorname{\textup{{sat}}}(\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ is in NP. Since $k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}\subseteq\textup{DQBF}_{\textup% {{cnf}}}^{\textup{{d}}}$ , $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ is also in NP for every constant $k$ .

For the NP-hardness, a reduction from $3$ -SAT to $3\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ can be done analogous to that of Theorem 8. A complete proof can be found in Section B.2. Since adding more existential variables only increases the complexity, $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ for every $k\geqslant 3$ and $\operatorname{\textup{{sat}}}(\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ are also NP-hard. $\hfill\blacktriangleleft$

4.4 $k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{$\alpha$}}}$ : Different Dependency Structure

It has been shown in [18] that $\operatorname{\textup{{sat}}}(\textup{DQBF}_{\textup{{cnf}}}^{\textup{{de}}})$ is $\mathrm{\Sigma_{3}^{P}}$ -complete and $\operatorname{\textup{{sat}}}(\textup{DQBF}_{\textup{{cnf}}}^{\textup{{dec}}})$ is NEXP-complete. Since $\textup{DQBF}_{\textup{{cnf}}}^{\textup{{dec}}}\subseteq\textup{DQBF}_{\textup% {{cnf}}}^{\textup{{ds}}}\subseteq\textup{DQBF}$ and $\operatorname{\textup{{sat}}}(\textup{DQBF})$ is also NEXP-complete, we know $\operatorname{\textup{{sat}}}(\textup{DQBF}_{\textup{{cnf}}}^{\textup{{ds}}})$ is NEXP-complete. In this section, we show a surprising result that, when $k$ is a constant, $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{$% \alpha$}}})$ has the same complexity as $k$ -SAT and $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ for every $\alpha\in\{\textup{{de}},\textup{{dec}},\textup{{ds}}\}$ . Since $k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}\subseteq k\textup{-DQBF}_{% \textup{{cnf}}}^{\textup{{de}}}\subseteq k\textup{-DQBF}_{\textup{{cnf}}}^{% \textup{{dec}}}\subseteq k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{ds}}}$ , it suffices to show the results for $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{ds}}})$ .

We start with $\operatorname{\textup{{sat}}}(2\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{ds}}})$ .

Theorem 15.

$\operatorname{\textup{{sat}}}(2\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{ds}}})$ is NL-complete.

Proof.

Since $2\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{ds}}}\supseteq 2\textup{-DQBF}_{% \textup{{cnf}}}^{\textup{{d}}}$ , the hardness follows from Theorem 8. For NL membership, consider a $2\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{ds}}}$ formula $\Phi\coloneqq\forall\bar{x},\exists y_{1}(D_{1}),\exists y_{2}(D_{2}).\,\varphi$ . First, we check whether $D_{1}$ and $D_{2}$ are disjoint using only logarithmic space. (See Remark 1.) If $D_{1}$ and $D_{2}$ are disjoint, we use the algorithm from Theorem 8 to determine its satisfiability. Otherwise, without loss of generality, we may assume that $D_{1}\subseteq D_{2}$ . We will show that this case can be decided in deterministic logarithmic space. Indeed, in this case $\Phi$ is a standard QBF and we can perform a level-ordered Q-resolution proof [16]. Since there are only two existential variables, any proof uses at most four clauses, and we can simply iterate through all $4$ -tuples of clause indices and check whether Q-resolution can be performed.

In the following, we give an alternative proof that works directly on the semantics of QBF. To ease notation, we write $\bar{z}_{1}\coloneqq D_{1}$ , $\bar{z}_{2}\coloneqq D_{2}\setminus D_{1}$ , and $\bar{z}_{3}\coloneqq\bar{x}\setminus D_{2}$ . Note that $\Phi$ is equivalent to a QBF

\begin{array}[]{RCL}\Psi&=&\forall\bar{z}_{1},\exists y_{1},\forall\bar{z}_{2}% ,\exists y_{2},\forall\bar{z}_{3}.\,\varphi\\ \hfil&=&\forall\bar{z}_{1},\exists y_{1},\forall\bar{z}_{2}.\,\left(\forall% \bar{z}_{3}.\,\varphi[\bot^{y_{2}}]\right)\vee\left(\forall\bar{z}_{3}.\,% \varphi[\top^{y_{2}}]\right)\\ \hfil&=&\forall\bar{z}_{1}.\,\left(\forall\bar{z}_{2}.\,\left(\forall\bar{z}_{% 3}.\,\varphi[(\bot^{y_{1}},\bot^{y_{2}})]\right)\vee\left(\forall\bar{z}_{3}.% \,\varphi[(\bot^{y_{1}},\top^{y_{2}})]\right)\right)\\ \hfil&\hfil&\phantom{\forall\bar{z}_{1}.\,}\vee\left(\forall\bar{z}_{2}.\,% \left(\forall\bar{z}_{3}.\,\varphi[(\top^{y_{1}},\bot^{y_{2}})]\right)\vee% \left(\forall\bar{z}_{3}.\,\varphi[(\top^{y_{1}},\top^{y_{2}})]\right)\right)% \,,\end{array}

which is false if and only if there are assignments $\bar{a}^{\bar{z}_{1}}$ , $\bar{b}^{\bar{z}_{2}}$ , and $\bar{c}^{\bar{z}_{2}}$ such that

	$\displaystyle\forall\bar{z}_{3}.\,\varphi[(\bot^{y_{1}},\bot^{y_{2}},\bar{a}^{% \bar{z}_{1}},\bar{b}^{\bar{z}_{2}})]\vee\forall\bar{z}_{3}.\,\varphi[(\bot^{y_% {1}},\top^{y_{2}},\bar{a}^{\bar{z}_{1}},\bar{b}^{\bar{z}_{2}})]\vee\forall\bar% {z}_{3}.\,\varphi[(\top^{y_{1}},\bot^{y_{2}},\bar{a}^{\bar{z}_{1}},\bar{c}^{% \bar{z}_{2}})]$
	$\displaystyle{}\vee\forall\bar{z}_{3}.\,\varphi[(\top^{y_{1}},\top^{y_{2}},% \bar{a}^{\bar{z}_{1}},\bar{c}^{\bar{z}_{2}})]$

is false. Since each of the four disjuncts is still in CNF, the formula is false if and only if each disjunct has a falsified clause. This is equivalent to finding four clauses $C_{1},C_{2},C_{3},C_{4}\in\varphi$ such that

$\blacksquare$

the clauses $C_{1},C_{2},C_{3},C_{4}$ are consistent on the variables in $\bar{z}_{1}$ ,
$\blacksquare$

the clauses $C_{1},C_{2}$ are consistent on the variables in $\bar{z}_{2}$ ,
$\blacksquare$

the clauses $C_{3},C_{4}$ are consistent on the variables in $\bar{z}_{2}$ , and
$\blacksquare$

$\neg C_{1}$ , $\neg C_{2}$ , $\neg C_{3}$ , and $\neg C_{4}$ are consistent with $\neg y_{1}\wedge\neg y_{2}$ , $\neg y_{1}\wedge y_{2}$ , $y_{1}\wedge\neg y_{2}$ , and $y_{1}\wedge y_{2}$ , respectively.

To find such clauses, we can iterate through all $4$ -tuples of clause indices and check whether the properties hold. $\hfill\blacktriangleleft$

Next, we show that for every $k\geqslant 3$ , $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{ds}}})$ is NP-complete, just like $k$ -SAT.

Theorem 16.

For every constant $k\geqslant 3$ , $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{ds}}})$ is NP-complete.

Before we present the proof of Theorem 16, we note that since $k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{de}}}\subseteq k\textup{-DQBF}_{% \textup{{cnf}}}^{\textup{{dec}}}\subseteq k\textup{-DQBF}_{\textup{{cnf}}}^{% \textup{{ds}}}$ , we obtain the following results as a corollary of Theorems 8, 14, 15, and 16.

Corollary 17.

$\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{de}}})$ and $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{dec}}})$ are NL-complete when $k=2$ and NP-complete when $k\geqslant 3$ .

The rest of this section is devoted to the proof of Theorem 16.

Proof of Theorem 16.

We will consider the membership proof. The hardness follows from Theorem 14. We fix a $k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{ds}}}$ formula:

\displaystyle\Phi\coloneqq\forall\bar{x},\exists y_{1}(D_{1}),\dots,\exists y_% {k}(D_{k}).\,\bigwedge_{j\in[m]}C_{j}.

(3)

Without loss of generality, we may assume that no existential variable has an empty dependency set, since our NP algorithm can guess an assignment to such variables at the outset. By Lemma 2, we may also assume that every universal variable appears in some dependency set. We say that a dependency set $D_{i}$ is maximal if there is no $j$ where $D_{i}\subsetneq D_{j}$ . An existential variable $y_{i}$ is maximal if its dependency set is maximal.

To decide the satisfiability of $\Phi$ , our algorithm works by recursion on the number of existential variables. The base case is when there is only one existential variable. This case can be decided in polynomial time and, in fact, in deterministic logspace. See, e.g., Theorem 19.

For the induction step, we pick a maximal variable $y_{t}$ . There are two cases.

Case 1: $D_{t}=\bar{x}$ .

We apply Lemma 3 and eliminate $y_{t}$ , resulting in a formula with one less existential variable and $O(m^{2})$ clauses. We then proceed recursively.

Case 2: $D_{t}\neq\bar{x}$ .

We deal with this case by generalising the technique in Lemma 13.

Let $\{i_{1},\ldots,i_{p}\}=\{i\nonscript\,|\allowbreak\nonscript\,\mathopen{}D_{i}% \subseteq D_{t}\}$ and $\{i_{1}^{\prime},\ldots,i_{q}^{\prime}\}=\{i^{\prime}\nonscript\,|\allowbreak% \nonscript\,\mathopen{}D_{i^{\prime}}\cap D_{t}=\emptyset\}$ . For each $j\in[m]$ , we partition $C_{j}$ into two clauses:

	$\displaystyle C_{j}^{+t}\coloneqq$	$\displaystyle\{\ell\nonscript\,\|\allowbreak\nonscript\,\mathopen{}% \operatorname{dep}(\ell)\subseteq D_{t}\}$
	$\displaystyle C_{j}^{-t}\coloneqq$	$\displaystyle C_{j}\setminus C_{j}^{+t}$

Intuitively, $C_{j}^{+t}$ is the subclause of $C_{j}$ that includes all the literals with dependency sets inside $D_{t}$ . On the other hand, $C_{j}^{-t}$ is the subclause that contains the rest of the literals. Due to the laminar structure of the dependency sets and that $y_{t}$ is a maximal variable, $C_{j}^{-t}=\{\ell\nonscript\,|\allowbreak\nonscript\,\mathopen{}\operatorname{% dep}(\ell)\cap D_{t}=\emptyset\}$ .

For a function $\xi:[m]\to\{+t,-t\}$ , we define two formulas:

	$\displaystyle\Phi_{+t,\xi}\coloneqq$	$\displaystyle\forall\bar{x},\exists y_{i_{1}}(D_{i_{1}}),\ldots,\exists y_{i_{% p}}(D_{i_{p}}).\ \bigwedge_{j:\xi(j)=+t}C_{j}^{+t}$
	$\displaystyle\Phi_{-t,\xi}\coloneqq$	$\displaystyle\forall\bar{x},\exists y_{i_{1}^{\prime}}(D_{i_{1}^{\prime}}),% \ldots,\exists y_{i_{q}^{\prime}}(D_{i_{q}^{\prime}}).\ \bigwedge_{j:\xi(j)=-t% }C_{j}^{-t}$

We have the following lemma.

Lemma 18.

$\Phi$ is satisfiable if and only if there is a function $\xi:[m]\to\{+t,-t\}$ such that $\Phi_{+t,\xi}$ and $\Phi_{-t,\xi}$ are both satisfiable.

Note that guessing $\xi$ requires $m$ bits. The algorithm guesses the function $\xi$ and verifies recursively that both $\Phi_{+t,\xi}$ and $\Phi_{-t,\xi}$ are satisfiable. Since the algorithm terminates after $k$ steps, and $k$ is a constant, and the number of clauses constructed in each recursive step is at most quadratically many, each step can be done in polynomial time. $\hfill\blacktriangleleft$

The proof of Lemma 18 is a generalisation of Lemma 11. Let $\bar{Y}$ be the vector of variables in the expansion $\exp(\Phi)$ . We can show that an assignment $\bar{a}$ on $\bar{Y}$ satisfies $\exp(\Phi)$ if and only if it satisfies $\exp(\Phi_{+t,\xi})$ and $\exp(\Phi_{-t,\xi})$ for some function $\xi$ . A detailed proof can be found in the appendix.

5 Complexity of $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}})$

In this section, we remove the constraint on the dependency structure and consider $k\textup{-DQBF}_{\textup{{cnf}}}$ . The case $k=1$ can be solved very efficiently.

Theorem 19.

$\operatorname{\textup{{sat}}}(1\textup{-DQBF}_{\textup{{cnf}}})$ is in L.

Proof.

Let $\Phi=\forall\bar{z}_{1},\bar{z}_{2},\exists y(\bar{z}_{1}).\,\bigwedge_{j\in[m% ]}C_{j}$ . Similar to the proof of Theorem 15, to show unsatisfiability, it suffices to find $C_{1},C_{2}\in\varphi$ such that

$\blacksquare$

$C_{1},C_{2}$ are consistent on the variables in $\bar{z}_{1}$ , and
$\blacksquare$

$\neg C_{1}$ and $\neg C_{2}$ are consistent with $\neg y$ and $y$ , respectively.

The correctness follows from the same reasoning. $\hfill\blacktriangleleft$

Next, we consider the case where $k=2$ .

Theorem 20.

$\operatorname{\textup{{sat}}}(2\textup{-DQBF}_{\textup{{cnf}}})$ is coNP-complete.

Proof.

For membership, we give an NP algorithm for checking unsatisfiability. Let $\Phi\coloneqq\forall\bar{x},\exists y_{1}(D_{1}),\exists y_{2}(D_{2}).\,\varphi$ be be a $2\textup{-DQBF}_{\textup{{cnf}}}$ formula. Let $\bar{z}=D_{1}\cap D_{2}$ . Note that for every assignment $\bar{a}$ on $\bar{z}$ , the induced formula $\Phi[\bar{a}]$ is a $2\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ formula, the satisfiability of which can be decided in polynomial time by Theorem 8. Therefore, to decide whether $\Phi$ is unsatisfiable, we can guess an assignment $\bar{a}$ on $\bar{z}$ and accept if and only if $\Phi[\bar{a}]$ is not satisfiable.

For hardness, we provide a reduction from the $3$ -DNF tautology problem to $\operatorname{\textup{{sat}}}(2\textup{-DQBF}_{\textup{{cnf}}})$ . Let $\varphi=\bigvee_{j\in[m]}Q_{j}$ be a 3-DNF formula over the variables $\bar{x}=(x_{1},\dots,x_{n})$ , where each $Q_{j}=(\ell_{j,1}\wedge\ell_{j,2}\wedge\ell_{j,3})$ is a $3$ -literal cube. We construct the following $2\textup{-DQBF}_{\textup{{cnf}}}$ formula:

\Psi=\forall\bar{x},\forall\bar{u}_{1},\forall\bar{u}_{2},\exists y_{1}(\bar{x% },\bar{u}_{1}),\exists y_{2}(\bar{x},\bar{u}_{2}).\,\psi_{1}\wedge\psi_{2}% \wedge\psi_{3}\wedge\psi_{4}\,,

where $\bar{u}_{1},\bar{u}_{2}$ have length $O(\log m)$ for representing the numbers in $[m]$ and $\psi_{1},\dots,\psi_{4}$ are as follows.

	$\displaystyle\psi_{1}\coloneqq$	$\displaystyle(\bar{u}_{1}=1)\rightarrow y_{1}$
	$\displaystyle\psi_{2}\coloneqq$	$\displaystyle\bigwedge_{j\in[m-1]}\Big{(}\big{(}(\bar{u}_{1}=j+1)\wedge(\bar{u% }_{2}=j)\big{)}\rightarrow(y_{2}\rightarrow y_{1})\big{)}$
	$\displaystyle\psi_{3}\coloneqq$	$\displaystyle\big{(}(\bar{u}_{1}=1)\wedge(\bar{u}_{2}=m)\big{)}\to(y_{2}% \rightarrow\neg y_{1})$
	$\displaystyle\psi_{4}\coloneqq$	$\displaystyle\bigwedge_{j\in[m]}\bigwedge_{i\in[3]}\Big{(}\big{(}(\bar{u}_{1}=% j)\wedge(\bar{u}_{2}=j)\wedge\neg\ell_{j,i}\big{)}\rightarrow(y_{1}\rightarrow y% _{2})\big{)}$

We claim that $\varphi$ is a tautology if and only if $\Psi$ is satisfiable. To see this, we fix an arbitrary assignment $\bar{a}$ on $\bar{x}$ and consider the induced formula $\Psi[\bar{a}]$ . Note that $\Psi[\bar{a}]$ is a $2\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ formula with universal variables $\bar{u}_{1},\bar{u}_{2}$ . Since $\lvert\bar{u}_{1}\rvert=\lvert\bar{u}_{2}\rvert=\log m$ , the expansion $\exp(\Psi[\bar{a}])$ is a 2-CNF formula with $2m$ variables $Y_{1,1},\dots,Y_{1,m},Y_{2,1},\dots,Y_{2,m}$ . Here we abuse the notation and write $Y_{i,j}$ instead of $Y_{i,\bar{a}}$ where $\bar{a}$ is the binary representation of $j$ .

It can be easily verified that the implication graph $G_{\bar{a}}$ of the expansion $\exp(\Psi[\bar{a}])$ is as shown in Figure 1, where a dashed edge $\overset{\scriptstyle\neg Q_{j}}{\dashrightarrow}$ is present if and only if $\bar{a}$ falsifies the cube $Q_{j}$ . Indeed, $\psi_{1}$ states that the edge $\neg Y_{1,1}\to Y_{1,1}$ is present. $\psi_{2}$ states that the edges $Y_{2,i}\to Y_{1,i+1}$ and $\neg Y_{1,i+1}\to\neg Y_{2,i}$ are present for every $i\in[m-1]$ . $\psi_{3}$ states that the edges $Y_{2,m}\to\neg Y_{1,1}$ and $Y_{1,1}\to\neg Y_{2,m}$ are present. Finally, $\psi_{4}$ states that the dashed edges $Y_{1,j}\overset{\scriptstyle\neg Q_{j}}{\dashrightarrow}Y_{2,j}$ and $Y_{1,j}\overset{\scriptstyle\neg Q_{j}}{\dashrightarrow}Y_{2,j}$ are present if $\bar{a}^{\bar{x}}$ falsifies $Q_{j}$ , for every $j\in[m]$ . This implies that $\bar{a}^{\bar{x}}$ falsifies all cubes in $\varphi$ if and only if there exists a cycle in $G_{\bar{a}}$ . Since a cycle in $G_{\bar{a}}$ (if exists) contains contradicting literals, $\bar{a}^{\bar{x}}$ falsifies all cubes in $\varphi$ if and only if $\Psi[\bar{a}]$ is not satisfiable. Since the assignment $\bar{a}$ is arbitrary, $\varphi$ is a tautology if and only if $\Psi$ is satisfiable. $\hfill\blacktriangleleft$

Figure 1: The implication graph

G_{\bar{a}}

. Each dashed edge

\overset{\neg Q_{i}}{\dashrightarrow}

is present if and only if

\bar{a}^{\bar{x}}

falsifies

Q_{i}

.

Next, we consider $k\textup{-DQBF}_{\textup{{cnf}}}$ . Note that $3\textup{-DQBF}_{\textup{{cnf}}}$ subsumes both $3\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ and $2\textup{-DQBF}_{\textup{{cnf}}}$ . Thus, $\operatorname{\textup{{sat}}}(3\textup{-DQBF}_{\textup{{cnf}}})$ is is both NP-hard and coNP-hard. We improve these results by showing that it is $\mathrm{\Pi_{2}^{P}}$ -hard.

Theorem 21.

$\operatorname{\textup{{sat}}}(3\textup{-DQBF}_{\textup{{cnf}}})$ is $\mathrm{\Pi_{2}^{P}}$ -hard.

Proof.

We show this by reduction from $\Pi_{2}$ -QBF in $3$ -CNF. The reduction is similar to the one in Theorem 14, except that the existential variables are allowed to depend on common variables, thereby enabling the encoding of a two-level QBF.

Let $\varphi=\forall\bar{z},\exists\bar{x}.\,\bigwedge_{j\in[m]}(\ell_{j,1}\vee\ell% _{j,2}\vee\ell_{j,3})$ be a $\Pi_{2}$ -QBF in $3$ -CNF. Let $\bar{x}=(x_{1},\dots,x_{n})$ and for a literal $\ell$ , let $\operatorname{ind}(\ell)$ denote the index $i$ where $x_{i}=\operatorname{var}(\ell)$ .

We construct the following $3\textup{-DQBF}_{\textup{{cnf}}}$ formula:

\Psi\coloneqq\forall\bar{z},\forall\bar{u}_{1},\forall\bar{u}_{2},\forall\bar{% u}_{3},\exists y_{1}(\bar{z},\bar{u}_{1}),\exists y_{2}(\bar{z},\bar{u}_{2}),% \exists y_{3}(\bar{z},\bar{u}_{3}).\,\psi_{1}\wedge\psi_{2}\wedge\psi_{3}\,,

where $\bar{u}_{1},\bar{u}_{2},\bar{u}_{3}$ have length $\log n$ for representing the variables in $\bar{x}$ and each $\psi_{1},\psi_{2},\psi_{3}$ is the following CNF formula:

	$\displaystyle\psi_{1}\coloneqq$	$\displaystyle\bigwedge_{i\in[n]}\Big{(}\big{(}(\bar{u}_{1}=i)\land(\bar{u}_{2}% =i)\big{)}\to(y_{1}\leftrightarrow y_{2})\big{)}$
	$\displaystyle\psi_{2}\coloneqq$	$\displaystyle\bigwedge_{i\in[n]}\Big{(}\big{(}(\bar{u}_{1}=i)\land(\bar{u}_{3}% =i)\big{)}\to(y_{1}\leftrightarrow y_{3})\big{)}$
	$\displaystyle\psi_{3}\coloneqq$	$\displaystyle\bigwedge_{j\in[m]}\Big{(}(\sigma_{j,1}\wedge\sigma_{j,2}\wedge% \sigma_{j,3})\rightarrow(\tau_{j,1}\vee\tau_{j,2}\vee\tau_{j,3}))\,,$

where for every $i\in[3]$ , $\sigma_{j,i}$ and $\tau_{j,i}$ are defined as

(\sigma_{j,i},\tau_{j,i})=\begin{dcases*}(\bar{u}_{i}=\operatorname{ind}(\ell_% {j,i}),y_{i}\leftrightarrow\operatorname{sgn}(\ell_{j,i}))&if $\operatorname{% var}(\ell_{j,i})$ is existential in $\varphi$\\ (\top,\ell_{j,i})&otherwise.\end{dcases*}

The intuition is that a vector of Skolem functions $f_{1},\dots,f_{n}$ for $\bar{x}$ in $\varphi$ can be encoded as a single function $g:\{\top,\bot\}^{|\bar{z}|}\times[n]\to\{\top,\bot\}$ , which then corresponds to a Skolem function for each $y_{i}$ in $\Psi$ . The formulas $\psi_{1}$ and $\psi_{2}$ state that for every Skolem functions $(g_{1},g_{2},g_{3})$ for $\Psi$ , all functions $g_{1},g_{2},g_{3}$ must be the same. Then, $\psi_{3}$ states that the Skolem functions $f_{1},\dots,f_{n}$ for $\varphi$ (if exists) must satisfies all the clauses $C_{1},\dots,C_{m}$ . Therefore, $\varphi$ is a true QBF if and only if $\Psi$ is satisfiable. $\hfill\blacktriangleleft$

We next show a Tseitin-like transformation that requires only three additional existential variables. This is in contrast with the standard Tseitin transformation that requires as many existential variables as the length of the input formula. Our new Tseitin-like transformation leads to new hardness results for $\operatorname{\textup{{sat}}}(5\textup{-DQBF}_{\textup{{cnf}}})$ and $\operatorname{\textup{{sat}}}(6\textup{-DQBF}_{\textup{{cnf}}})$ .

Lemma 22 (Reformulated Tseitin Transformation).

Given a $k\textup{-DQBF}$ formula, we can construct in polynomial time an equisatisfiable $(k+3)\textup{-DQBF}_{\textup{{cnf}}}$ formula.

Proof.

Let $\Phi=\forall\bar{x},\exists y_{1}(\bar{z}_{1}),\dots,\exists y_{k}(\bar{z}_{k}% ).\,\varphi$ be a $k\textup{-DQBF}$ formula where $\varphi$ is a circuit with gates $g_{1},\dots,g_{m}$ . We assume, without loss of generality, that

g_{i}=\begin{dcases*}x_{i}&for every $1\leqslant i\leqslant n$\\ y_{i-n}&for every $n+1\leqslant i\leqslant n+k$\\ f_{i}(g_{l_{i}},g_{r_{i}})&for every $n+k+1\leqslant i\leqslant m$,\end{dcases*}

where $l_{i},r_{i}\in[i-1]$ are the indices of the two fan-ins of the gate $g_{i}$ implementing the Boolean function $f_{i}$ , and that $g_{m}$ corresponds to the primary output of the circuit.

We construct the $(k+3)\textup{-DQBF}_{\textup{{cnf}}}$ formula

\Psi\coloneqq\forall\bar{x},\forall\bar{u}_{1},\forall\bar{u}_{2},\forall\bar{% u}_{3},\exists y_{1}(\bar{z}_{1}),\dots,\exists y_{k}(\bar{z}_{k}),\exists t_{% 1}(\bar{x},\bar{u}_{1}),\exists t_{2}(\bar{x},\bar{u}_{2}),\exists t_{3}(\bar{% x},\bar{u}_{3}).\,\psi\,,

where $\bar{u}_{1},\bar{u}_{2},\bar{u}_{3}$ have length $\log m$ for representing the numbers in $[m]$ and $\psi$ is a CNF formula with clauses encoding

$\blacksquare$

$((\bar{u}_{1}=i)\wedge(\bar{u}_{2}=i))\to(t_{1}\leftrightarrow t_{2})$ for every $i\in[m]$ ,
$\blacksquare$

$((\bar{u}_{1}=i)\wedge(\bar{u}_{3}=i))\to(t_{1}\leftrightarrow t_{3})$ for every $i\in[m]$ ,
$\blacksquare$

$(\bar{u}_{1}=i)\to(t_{1}\leftrightarrow x_{i})$ for every $i\in[n]$ ,
$\blacksquare$

$(\bar{u}_{1}=n+i)\to(t_{1}\leftrightarrow y_{i})$ for every $i\in[k]$ ,
$\blacksquare$

$((\bar{u}_{1}=i)\land(\bar{u}_{2}=l_{i})\land(\bar{u}_{3}=r_{i}))\to(t_{1}% \leftrightarrow f_{i}(t_{2},t_{3}))$ for every $n+k+1\leqslant i\leqslant m$ ,
$\blacksquare$

$(\bar{u}_{1}=m)\to t_{1}$ .

The intuitive meaning is as follows. The first two items state that the Skolem functions for $t_{1},t_{2},t_{3}$ must be the same. The next three state that the Skolem function $g$ for $t_{1}$ encodes the values of the gates, where $g(\bar{x},\bar{u}_{1})$ is the value of gate $j$ when $\bar{u}_{1}$ is the binary representation of $j$ . The last item encodes that the output of the circuit must be true. The correctness proof is routine and hence omitted. $\hfill\blacktriangleleft$

In particular, by combining Lemma 22 with the fact that $\operatorname{\textup{{sat}}}(2\textup{-DQBF})$ and $\operatorname{\textup{{sat}}}(3\textup{-DQBF})$ are PSPACE-complete and NEXP-complete [14], we establish the hardness of $\operatorname{\textup{{sat}}}(5\textup{-DQBF}_{\textup{{cnf}}})$ and $\operatorname{\textup{{sat}}}(6\textup{-DQBF}_{\textup{{cnf}}})$ .

Theorem 23.

$\operatorname{\textup{{sat}}}(5\textup{-DQBF}_{\textup{{cnf}}})$ is PSPACE-hard and $\operatorname{\textup{{sat}}}(6\textup{-DQBF}_{\textup{{cnf}}})$ is NEXP-complete.

6 Conclusions and Future Work

While $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{dnf}}}^{\textup{{d}}})$ is as hard as $\operatorname{\textup{{sat}}}(k\textup{-DQBF})$ , we observe a range of differing complexity results in the CNF case. For the case of $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ , we show that it is in fact as easy as $k$ -SAT – exponentially easier than $\operatorname{\textup{{sat}}}(k\textup{-DQBF})$ . Generalising the results in [18], we also show that $\operatorname{\textup{{sat}}}(\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$ is NP-complete and that $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{$% \alpha$}}})$ has the same complexity as $k$ -SAT for $\alpha\in\{\textup{{d}},\textup{{de}},\textup{{dec}},\textup{{ds}}\}$ . For the case of $k\textup{-DQBF}_{\textup{{cnf}}}$ , we show that it is only coNP-complete when $k=2$ (whereas $\operatorname{\textup{{sat}}}(2\textup{-DQBF})$ is PSPACE-complete) and of the same NEXP-complete complexity as $\operatorname{\textup{{sat}}}(\textup{DQBF})$ when $k\geqslant 6$ . These results show that, when parametrising DQBF with the number of existential variables, it is more natural to consider DNF as the normal form for the matrix, analogous to how CNF is considered the standard form for SAT.

The exact complexity of $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}})$ is yet to be discovered for $k=3$ , $4$ , and $5$ . In particular, the best-known membership result is still that they are in NEXP. We leave this for future work.

References

[1] Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Inf. Process. Lett., 8(3):121–123, 1979. doi:10.1016/0020-0190(79)90002-4.
[2] V. Balabanov and J.-H. R. Jiang. Reducing satisfiability and reachability to DQBF. In QBF Workshop, 2015.
[3] Valeriy Balabanov, Hui-Ju Katherine Chiang, and Jie-Hong R. Jiang. Henkin quantifiers and Boolean formulae: A certification perspective of DQBF. Theoretical Computer Science, 523:86–100, 2014. doi:10.1016/j.tcs.2013.12.020.
[4] Armin Biere, Mathias Fleury, Nils Froleyks, and Marijn J. H. Heule. The SAT museum. In Matti Järvisalo and Daniel Le Berre, editors, Proceedings of the 14th International Workshop on Pragmatics of SAT, volume 3545, pages 72–87. CEUR-WS.org, 2023. URL: https://ceur-ws.org/Vol-3545/paper6.pdf.
[5] Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185. IOS Press, 2009.
[6] Uwe Bubeck. Model-Based Transformations for Quantified Boolean Formulas. PhD thesis, University of Paderborn, 2010.
[7] Uwe Bubeck and Hans Kleine Büning. Dependency quantified Horn formulas: Models and complexity. In Armin Biere and Carla P. Gomes, editors, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, volume 4121, pages 198–211. Springer, 2006. doi:10.1007/11814948_21.
[8] Uwe Bubeck and Hans Kleine Büning. Rewriting (dependency-)quantified 2-CNF with arbitrary free literals into existential 2-HORN. In Ofer Strichman and Stefan Szeider, editors, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, volume 6175, pages 58–70. Springer, 2010. doi:10.1007/978-3-642-14186-7_7.
[9] Fa-Hsun Chen, Shen-Chang Huang, Yu-Cheng Lu, and Tony Tan. Reducing NEXP-complete problems to DQBF. In Alberto Griggio and Neha Rungta, editors, Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, pages 199–204, 2022. doi:10.34727/2022/isbn.978-3-85448-053-2_26.
[10] Johannes Klaus Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. The silent (r)evolution of SAT. Commun. ACM, 66(6):64–72, 2023. doi:10.1145/3560469.
[11] Ana Paulina Figueroa and Bernardo Llano. An infinite family of self-diclique digraphs. Appl. Math. Lett., 23(5):630–632, 2010. doi:10.1016/j.aml.2010.01.026.
[12] Andreas Fröhlich, Gergely Kovásznai, Armin Biere, and Helmut Veith. iDQ: Instantiation-based DQBF solving. In Proceedings of the Fifth Pragmatics of SAT workshop, volume 27, pages 103–116, 2014. doi:10.29007/1s5k.
[13] Long-Hin Fung, Che Cheng, Yu-Wei Fan, Tony Tan, and Jie-Hong Roland Jiang. 2-DQBF solving and certification via property-directed reachability analysis. In Proceedings of the Conference on Formal Methods in Computer-Aided Design, pages 197–207. IEEE, 2024. doi:10.34727/2024/isbn.978-3-85448-065-5_25.
[14] Long-Hin Fung and Tony Tan. On the complexity of $k$ -DQBF. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, volume 271, pages 10:1–10:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.SAT.2023.10.
[15] Robert Ganian, Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Fixed-parameter tractability of dependency QBF with structural parameters. In Diego Calvanese, Esra Erdem, and Michael Thielscher, editors, Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece, September 12-18, 2020, pages 392–402, 2020. doi:10.24963/kr.2020/40.
[16] Mikolás Janota and João Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577(C):25–42, 2015. doi:10.1016/j.tcs.2015.01.048.
[17] G. Peterson, J. Reif, and S. Azhar. Lower bounds for multiplayer noncooperative games of incomplete information. Computers & Mathematics with Applications, 41(7):957–992, 2001. doi:10.1016/S0898-1221(00)00333-3.
[18] Christoph Scholl, Jie-Hong Roland Jiang, Ralf Wimmer, and Aile Ge-Ernst. A PSPACE subclass of dependency quantifed Boolean formulas and its effective solving. In Proceedings of the AAAI Conference on Artificial Intelligence, pages 1584–1591. AAAI Press, 2019. doi:10.1609/aaai.v33i01.33011584.
[19] G. Tseitin. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part II, 1968.
[20] Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, and Bernd Becker. Preprocessing for DQBF. In Marijn Heule and Sean A. Weaver, editors, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, volume 9340, pages 173–190, Cham, 2015. Springer International Publishing. doi:10.1007/978-3-319-24318-4_13.
[21] Lintao Zhang. Solving QBF with combined conjunctive and disjunctive normal form. In Proceedings of the 21st National Conference on Artificial Intelligence, pages 143–150. AAAI Press, 2006. URL: http://www.aaai.org/Library/AAAI/2006/aaai06-023.php.

Appendix A Additional Background

We provide additional background knowledge in this section.

A.1 Tseitin Transformation

Tseitin transformation is a standard technique to turn an arbitrary Boolean satisfiability problem into an equisatisfiable one in $3$ -CNF form [19]. It can be directly lifted to QBF and DQBF by allowing the Tseitin variables to depend on every universal variable.

Given a DQBF

\Phi=\forall\bar{x},\exists y_{1}(\bar{z}_{1}),\dots,\exists y_{k}(\bar{z}_{k}% ).\,\varphi\,,

where $\varphi$ is a circuit with gates $g_{1},\dots,g_{m}$ , we assume, without loss of generality, that

g_{i}=\begin{dcases*}x_{i}&for every $1\leqslant i\leqslant n$\\ y_{i-n}&for every $n+1\leqslant i\leqslant n+k$\\ f_{i}(g_{l_{i}},g_{r_{i}})&for every $n+k+1\leqslant i\leqslant m$,\end{dcases*}

where $l_{i},r_{i}\in[i-1]$ are the indices of the two fanins of the gate $g_{i}$ implementing the Boolean function $f_{i}$ .

The core idea of Tseitin transformation is that we can introduce a fresh variable $t_{i}$ for every gate $g_{i}$ and encode locally the relation between the inputs and the output of the gate. The formula $\psi_{G}$ encoding these constraints is a CNF formula encoding

$\blacksquare$

$t_{i}\leftrightarrow x_{i}$ for every $1\leqslant i\leqslant n$ ,
$\blacksquare$

$t_{i}\leftrightarrow y_{i-n}$ for every $n+1\leqslant i\leqslant n+k$ , and
$\blacksquare$

$t_{i}\leftrightarrow f_{i}(t_{l_{i}},t_{r_{i}})$ for every $n+k+1\leqslant i\leqslant m$ .

We then have $\Phi$ is equisatisfiable to

\Psi_{1}\coloneqq\forall\bar{x},\exists y_{1}(\bar{z}_{1}),\dots,\exists y_{k}% (\bar{z}_{k}),\exists\bar{t}(\bar{x}).\,\psi_{G}\wedge t_{m}\,.

To transform it to DNF form, as noted in [9], $\Phi$ is equisatisfiable to

\Psi_{2}\coloneqq\forall\bar{x},\forall\bar{t},\exists y_{1}(\bar{z}_{1}),% \dots,\exists y_{k}(\bar{z}_{k}).\,\psi_{G}\rightarrow t_{m}\,.

Note that the matrix of the formula is in DNF form. In the context of QBF, it can be thought of as applying the Tseitin transformation on $\neg\varphi$ and then negating the resulting existential formula [21]. We refer to this as the DNF version of Tseitin transformation.

Appendix B Omitted Proofs

We fill in the omitted proofs in the main text in this section.

B.1 Complexity of $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{dnf}}}^{\textup{{d}}})$

Proof of Theorem 4.

Since we are considering subclasses of $k\textup{-DQBF}$ , it suffices to show the hardness part.

First, observe that the DNF version of the Tseitin transformation (see Section A.1) preserves both the number of existential variables and the dependency structure. Therefore, we have that $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{dnf}}}^{\textup{{$% \alpha$}}})$ is as hard as $\operatorname{\textup{{sat}}}(k\textup{-DQBF}^{\textup{{$\alpha$}}})$ for every combination of $\alpha$ and $k$ . In addition, observe that the formula constructed to show the PSPACE- and NEXP-hardness of $\operatorname{\textup{{sat}}}(2\textup{-DQBF})$ and $\operatorname{\textup{{sat}}}(3\textup{-DQBF})$ in [14, Theorems 4 and 5] are in fact $2\textup{-DQBF}^{\textup{{d}}}$ and $3\textup{-DQBF}^{\textup{{d}}}$ , respectively. Thus, we have $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{dnf}}}^{\textup{{d}}})$ is coNP-, PSPACE-, and NEXP-complete for $k=1$ , $k=2$ , and $k\geqslant 3$ , respectively. $\hfill\blacktriangleleft$

B.2 Hardness of $\operatorname{\textup{{sat}}}(3\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$

Hardness Proof of Theorem 14.

Let $\varphi=\bigwedge_{j\in[m]}(\ell_{j,1}\vee\ell_{j,2}\vee\ell_{j,3})$ be a $3$ -CNF formula over the variables $\bar{x}=(x_{i})_{i\in[n]}$ . We again write $\operatorname{ind}(\ell)\coloneqq i$ if $\operatorname{var}(\ell)=x_{i}$ .

We construct the following $3\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ formula

\Psi\coloneqq\forall\bar{u}_{1},\forall\bar{u}_{2},\forall\bar{u}_{3},\exists y% _{1}(\bar{u}_{1}),\exists y_{2}(\bar{u}_{2}),\exists y_{3}(\bar{u}_{3}).\,\psi\,,

where $\bar{u}_{1}$ , $\bar{u}_{2}$ , and $\bar{u}_{3}$ are of length $O(\log n)$ for representing the variables in $\bar{x}$ and $\psi$ is a CNF formula that states the following.

$\blacksquare$

$(\bar{u}_{1}=i)\land(\bar{u}_{2}=i)\to(y_{1}\leftrightarrow y_{2})$ for every $i\in[n]$ ,
$\blacksquare$

$(\bar{u}_{1}=i)\land(\bar{u}_{3}=i)\to(y_{1}\leftrightarrow y_{3})$ for every $i\in[n]$ , and
$\blacksquare$

$(\bar{u}_{1}=\operatorname{ind}(\ell_{j,1}))\land(\bar{u}_{2}=\operatorname{% ind}(\ell_{j,2}))\land(\bar{u}_{3}=\operatorname{ind}(\ell_{j,3}))\to(y_{1}% \leftrightarrow\operatorname{sgn}(\ell_{j,1}))\lor(y_{2}\leftrightarrow% \operatorname{sgn}(\ell_{j,2}))\lor(y_{3}\leftrightarrow\operatorname{sgn}(% \ell_{j,3}))$ for every $j\in[m]$ .

The first two items state that the Skolem functions for $y_{1}$ , $y_{2}$ , and $y_{3}$ must be the same. The third item implies that $\bar{a}^{\bar{x}}$ is a satisfying assignment of $\varphi$ if and only if the function $f_{\bar{a}}$ is a Skolem function for $\Psi$ by encoding $\bar{a}^{\bar{x}}$ as a function $f_{\bar{a}}\colon[n]\to\{\top,\bot\}$ , where $f_{\bar{a}}(i)=\bar{a}^{\bar{x}}(x_{i})$ . $\hfill\blacktriangleleft$

B.3 Proof of Lemma 18

Recall that we fix a $k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{ds}}}$ formula:

\displaystyle\addcontentsline{lla}{section}{\numberline{\string\crtrefnumber{% eq:not-f-dqbf}}{e}q:not-f-dqbf}\Phi\coloneqq\forall\bar{x},\exists y_{1}(D_{1}% ),\dots,\exists y_{k}(D_{k}).\,\bigwedge_{j\in[m]}C_{j}.

(4)

Let $\bar{y}=(y_{1},\dots,y_{k})$ . We recall some of the notation used in the main text.

$\blacksquare$

$y_{t}$ is a maximal variable where $D_{t}\neq\bar{x}$ .
$\blacksquare$

$\{i_{1},\ldots,i_{p}\}=\{i\nonscript\,|\allowbreak\nonscript\,\mathopen{}D_{i}% \subseteq D_{t}\}$ and $\{i_{1}^{\prime},\ldots,i_{q}^{\prime}\}=\{i^{\prime}\nonscript\,|\allowbreak% \nonscript\,\mathopen{}D_{i^{\prime}}\cap D_{t}=\emptyset\}$ .
$\blacksquare$

For each $j\in[m]$ :

$\displaystyle C_{j}^{+t}\coloneqq$ $\displaystyle\{\ell\nonscript\,|\allowbreak\nonscript\,\mathopen{}% \operatorname{dep}(\ell)\subseteq D_{t}\}$

$\displaystyle C_{j}^{-t}\coloneqq$ $\displaystyle C_{j}\setminus C_{j}^{+t}$
$\blacksquare$

For a function $\xi:[m]\to\{+t,-t\}$ , we define two formulas:

$\displaystyle\Phi_{+t,\xi}\coloneqq$ $\displaystyle\forall\bar{x},\exists y_{i_{1}}(D_{i_{1}}),\ldots,\exists y_{i_{% p}}(D_{i_{p}}).\ \bigwedge_{j\ \text{s.t.}\ \xi(j)=+t}C_{j}^{+t}$

$\displaystyle\Phi_{-t,\xi}\coloneqq$ $\displaystyle\forall\bar{x},\exists y_{i_{1}^{\prime}}(D_{i_{1}^{\prime}}),% \ldots,\exists y_{i_{q}^{\prime}}(D_{i_{q}^{\prime}}).\ \bigwedge_{j\ \text{s.% t.}\ \xi(j)=-t}C_{j}^{-t}$

Finally, we recall Lemma 18.

See 18

To prove Lemma 18, we will need additional notation and terminology. Let $S_{t}\coloneqq\{y_{i}\nonscript\,|\allowbreak\nonscript\,\mathopen{}D_{i}% \subseteq D_{t}\}$ . Note that $y_{t}\in S_{t}$ . To ease notation, we write $D_{t}^{c}:=\bar{x}\setminus D_{t}$ and $S_{t}^{c}:=\bar{y}\setminus S_{t}$ . That is, $D_{t}^{c}$ is the complement of $D_{t}$ w.r.t. $\bar{x}$ and $S_{t}^{c}$ is the complement of $S_{t}$ w.r.t. $\bar{y}$ . In the following, we will drop the subscript $t$ in $D_{t},S_{t},D_{t}^{c},S_{t}^{c}$ and simply write $D,S,D^{c},S^{c}$ .

For an assignment $(\bar{a}^{D},\bar{b}^{S})$ , we define the clause $\operatorname{cl}(\bar{a}^{D},\bar{b}^{S})$ :

\operatorname{cl}(\bar{a}^{D},\bar{b}^{S})\ \coloneqq\ \bigvee_{i\in S}Y_{i,% \bar{a}_{i}}\oplus b_{i},\qquad\quad\text{where each}\ \bar{a}_{i}=\bar{a}^{D}% (D_{i})\ \text{and}\ b_{i}=\bar{b}^{S}(y_{i}).

Similarly, for an assignment $(\bar{a}^{D^{c}},\bar{b}^{S^{c}})$ , we define the clause $\operatorname{cl}(\bar{a}^{D^{c}},\bar{b}^{S(y)^{c}})$ :

\operatorname{cl}(\bar{a}^{D^{c}},\bar{b}^{S^{c}})\ \coloneqq\bigvee_{y_{i}\in S% ^{c}}Y_{i,\bar{a}_{i}}\oplus b_{i},\qquad\quad\text{where each}\ \bar{a}_{i}=% \bar{a}^{D^{c}}(D_{i})\ \text{and}\ b_{i}=\bar{b}^{S^{c}}(y_{i}).

We now generalise Definition 6 to the laminar case.

Definition 24.

Let $\Phi$ be as in Equation 4. For every $j\in[m]$ , we define the sets:

	$\displaystyle\mathcal{L}_{+t,j}^{\ast}(\Phi)\coloneqq$	$\displaystyle\{\operatorname{cl}(\bar{a}^{D},\bar{b}^{S})\nonscript\,\|% \allowbreak\nonscript\,\mathopen{}(\bar{a}^{D},\bar{b}^{S})\simeq\neg C_{j}^{+% t}\}$
	$\displaystyle\mathcal{L}_{-t,j}^{\ast}(\Phi)\coloneqq$	$\displaystyle\{\operatorname{cl}(\bar{a}^{D^{c}},\bar{b}^{S^{c}})\nonscript\,\|% \allowbreak\nonscript\,\mathopen{}(\bar{a}^{D^{c}},\bar{b}^{S^{c}})\simeq\neg C% _{j}^{-t}\}$
	$\displaystyle\mathfrak{C}_{j}(\Phi)\coloneqq$	$\displaystyle\left\{\mathcal{C}_{\bar{a},\bar{b}}\nonscript\,\middle\|% \allowbreak\nonscript\,\mathopen{}(\bar{a}^{\bar{x}},\bar{b}^{\bar{y}})\simeq% \neg C_{j}\right\}$

The following lemma is a generalisation of Lemma 7 to the laminar case.

Lemma 25.

Let $\Phi$ be as in Equation 4. Then, for every $j\in[m]$ , $\mathfrak{C}_{j}=\mathcal{L}_{+t,j}^{\ast}(\Phi)\times\mathcal{L}_{-t,j}^{\ast% }(\Phi)$ .

Proof.

The proof is a straightforward generalisation of Lemma 7. For the sake of completeness, we present it here.

We fix an arbitrary $j\in[m]$ . We first prove the “ $\subseteq$ ” direction. Let $\mathcal{C}_{\bar{a},\bar{b}}$ be a clause in $\mathfrak{C}_{j}$ . That is, $(\bar{a}^{\bar{x}},\bar{b}^{\bar{y}})$ is an assignment that falsifies $C_{j}$ . By definition, $\mathcal{C}_{\bar{a},\bar{b}}=\bigvee_{i\in[k]}Y_{i,\bar{a}_{i}}\oplus b_{i}$ . Since $(\bar{a},\bar{b})$ falsifies $C_{j}$ , it is consistent with the cube $\neg C_{j}$ .

Let $\bar{a}_{t}=\bar{a}^{\bar{x}}(D)$ and $\bar{b}_{t}=\bar{b}^{\bar{y}}(S)$ . Let $\bar{a}_{0}=\bar{a}^{\bar{x}}(D^{c})$ and $\bar{b}_{0}=\bar{b}^{\bar{y}}(S^{c})$ . Both are consistent with the cubes $\neg C_{j}^{+t}$ and $\neg C_{j}^{-t}$ , respectively. By definition, the clause $\operatorname{cl}(\bar{a}_{t}^{D},\bar{b}_{t}^{S})$ is in $\mathcal{L}_{+t,j}^{\ast}(\Phi)$ and the clause $\operatorname{cl}(\bar{a}_{t}^{D^{c}},\bar{b}_{t}^{S^{c}})$ is in $\mathcal{L}_{-t,j}^{\ast}(\Phi)$ . The inclusion follows since

\mathcal{C}_{\bar{a},\bar{b}}=\operatorname{cl}(\bar{a}_{t}^{D},\bar{b}_{t}^{S% })\ \vee\ \operatorname{cl}(\bar{a}_{t}^{D^{c}},\bar{b}_{t}^{S^{c}})

Next, we prove the “ $\supseteq$ ” direction. Let $C\in\mathcal{L}_{+t,j}^{\ast}(\Phi)\times\mathcal{L}_{-t,j}^{\ast}(\Phi)$ . Let $C\coloneqq B_{1}\vee B_{2}$ , where $B_{1}\in\mathcal{L}_{+t,j}^{\ast}(\Phi)$ and $B_{2}\in\mathcal{L}_{-t,j}^{\ast}(\Phi)$ . By definition,

$\blacksquare$

there is assignment $(\bar{a}_{1}^{D},\bar{b}_{1}^{S})$ such that $B_{1}$ is the clause $\operatorname{cl}(\bar{a}_{1}^{D},\bar{b}_{1}^{S})$ ,
$\blacksquare$

there is assignment $(\bar{a}_{2}^{D^{c}},\bar{b}_{2}^{S^{c}})$ such that $B_{2}$ is the clause $\operatorname{cl}(\bar{a}_{2}^{D^{c}},\bar{b}_{2}^{S^{c}})$ .

Since the dependency sets of the variables in $S$ are disjoint with the dependency sets of the variables in $S^{c}$ , the assignments $(\bar{a}_{1}^{D},\bar{b}_{1}^{S})$ and $(\bar{a}_{2}^{D^{c}},\bar{b}_{2}^{S^{c}})$ are consistent. Let $(\bar{a}^{\bar{x}},\bar{b}^{\bar{y}})$ be their union, which is consistent with $\neg C_{j}^{+t}\wedge\neg C_{j}^{-t}$ . Therefore, $(\bar{a}^{\bar{x}},\bar{b}^{\bar{y}})$ is a falsifying assignment of $C_{j}$ . By definition, the clause $\mathcal{C}_{\bar{a},\bar{b}}=B_{1}\vee B_{2}$ and it is in $\mathfrak{C}_{j}$ . $\hfill\blacktriangleleft$

Now, Lemma 18 follows from the following lemma, which is the generalisation of Lemma 11.

Lemma 26.

Let $\Phi$ be as in Equation 4 and let $\bar{Y}$ be the vector of variables in $\exp(\Phi)$ . For every assignment $\bar{a}^{\bar{Y}}$ , $\bar{a}^{\bar{Y}}$ satisfies $\exp(\Phi)$ if and only if it satisfies $\exp(\Phi_{+t,\xi})$ and $\exp(\Phi_{-t,\xi})$ for some function $\xi:[m]\to\{+t,-t\}$ .

Proof.

The proof is similar to Lemma 26. For completeness, we reprove it here. We observe that:

	$\displaystyle\exp(\Phi)=$	$\displaystyle\bigwedge_{j\in[m]}\bigwedge_{C\in\mathfrak{C}_{j}}C$
	$\displaystyle=$	$\displaystyle\bigwedge_{j\in[m]}\quad\bigwedge_{(C_{1},C_{2})\in\mathcal{L}_{+% t,j}^{\ast}(\Phi)\times\mathcal{L}_{-t,j}^{\ast}(\Phi)}C_{1}\vee C_{2}$

The second equality comes from Lemma 25. Thus, $\exp(\Phi)$ is satisfiable iff there is a function $\xi:[m]\to\{+t,-t\}$ such that

\left(\bigwedge_{j:\xi(j)=+t}\,\bigwedge_{C_{1}\in\mathcal{L}_{+t,j}^{\ast}(% \Phi)}C_{1}\right)\wedge\left(\bigwedge_{j:\xi(j)=-t}\,\bigwedge_{C_{2}\in% \mathcal{L}_{-t,j}^{\ast}(\Phi)}C_{2}\right)

is satisfiable. The first part of the conjunction is precisely $\exp(\Phi_{+t,\xi})$ and the second part is precisely $\exp(\Phi_{-t,\xi})$ . $\hfill\blacktriangleleft$

[bib.bib1] [1] Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Inf. Process. Lett., 8(3):121–123, 1979. doi:10.1016/0020-0190(79)90002-4.

[bib.bib2] [2] V. Balabanov and J.-H. R. Jiang. Reducing satisfiability and reachability to DQBF. In QBF Workshop, 2015.

[bib.bib3] [3] Valeriy Balabanov, Hui-Ju Katherine Chiang, and Jie-Hong R. Jiang. Henkin quantifiers and Boolean formulae: A certification perspective of DQBF. Theoretical Computer Science, 523:86–100, 2014. doi:10.1016/j.tcs.2013.12.020.

[bib.bib4] [4] Armin Biere, Mathias Fleury, Nils Froleyks, and Marijn J. H. Heule. The SAT museum. In Matti Järvisalo and Daniel Le Berre, editors, Proceedings of the 14th International Workshop on Pragmatics of SAT, volume 3545, pages 72–87. CEUR-WS.org, 2023. URL: https://ceur-ws.org/Vol-3545/paper6.pdf.

[bib.bib5] [5] Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185. IOS Press, 2009.

[bib.bib6] [6] Uwe Bubeck. Model-Based Transformations for Quantified Boolean Formulas. PhD thesis, University of Paderborn, 2010.

[bib.bib7] [7] Uwe Bubeck and Hans Kleine Büning. Dependency quantified Horn formulas: Models and complexity. In Armin Biere and Carla P. Gomes, editors, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, volume 4121, pages 198–211. Springer, 2006. doi:10.1007/11814948_21.

[bib.bib8] [8] Uwe Bubeck and Hans Kleine Büning. Rewriting (dependency-)quantified 2-CNF with arbitrary free literals into existential 2-HORN. In Ofer Strichman and Stefan Szeider, editors, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, volume 6175, pages 58–70. Springer, 2010. doi:10.1007/978-3-642-14186-7_7.

[bib.bib9] [9] Fa-Hsun Chen, Shen-Chang Huang, Yu-Cheng Lu, and Tony Tan. Reducing NEXP-complete problems to DQBF. In Alberto Griggio and Neha Rungta, editors, Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, pages 199–204, 2022. doi:10.34727/2022/isbn.978-3-85448-053-2_26.

[bib.bib10] [10] Johannes Klaus Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. The silent (r)evolution of SAT. Commun. ACM, 66(6):64–72, 2023. doi:10.1145/3560469.

[bib.bib11] [11] Ana Paulina Figueroa and Bernardo Llano. An infinite family of self-diclique digraphs. Appl. Math. Lett., 23(5):630–632, 2010. doi:10.1016/j.aml.2010.01.026.

[bib.bib12] [12] Andreas Fröhlich, Gergely Kovásznai, Armin Biere, and Helmut Veith. iDQ: Instantiation-based DQBF solving. In Proceedings of the Fifth Pragmatics of SAT workshop, volume 27, pages 103–116, 2014. doi:10.29007/1s5k.

[bib.bib13] [13] Long-Hin Fung, Che Cheng, Yu-Wei Fan, Tony Tan, and Jie-Hong Roland Jiang. 2-DQBF solving and certification via property-directed reachability analysis. In Proceedings of the Conference on Formal Methods in Computer-Aided Design, pages 197–207. IEEE, 2024. doi:10.34727/2024/isbn.978-3-85448-065-5_25.

[bib.bib14] [14] Long-Hin Fung and Tony Tan. On the complexity of $k$ -DQBF. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, volume 271, pages 10:1–10:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.SAT.2023.10.

[bib.bib15] [15] Robert Ganian, Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Fixed-parameter tractability of dependency QBF with structural parameters. In Diego Calvanese, Esra Erdem, and Michael Thielscher, editors, Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece, September 12-18, 2020, pages 392–402, 2020. doi:10.24963/kr.2020/40.

[bib.bib16] [16] Mikolás Janota and João Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577(C):25–42, 2015. doi:10.1016/j.tcs.2015.01.048.

[bib.bib17] [17] G. Peterson, J. Reif, and S. Azhar. Lower bounds for multiplayer noncooperative games of incomplete information. Computers & Mathematics with Applications, 41(7):957–992, 2001. doi:10.1016/S0898-1221(00)00333-3.

[bib.bib18] [18] Christoph Scholl, Jie-Hong Roland Jiang, Ralf Wimmer, and Aile Ge-Ernst. A PSPACE subclass of dependency quantifed Boolean formulas and its effective solving. In Proceedings of the AAAI Conference on Artificial Intelligence, pages 1584–1591. AAAI Press, 2019. doi:10.1609/aaai.v33i01.33011584.

[bib.bib19] [19] G. Tseitin. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part II, 1968.

[bib.bib20] [20] Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, and Bernd Becker. Preprocessing for DQBF. In Marijn Heule and Sean A. Weaver, editors, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, volume 9340, pages 173–190, Cham, 2015. Springer International Publishing. doi:10.1007/978-3-319-24318-4_13.

[bib.bib21] [21] Lintao Zhang. Solving QBF with combined conjunctive and disjunctive normal form. In Proceedings of the 21st National Conference on Artificial Intelligence, pages 143–150. AAAI Press, 2006. URL: http://www.aaai.org/Library/AAAI/2006/aaai06-023.php.

Fine-Grained Complexity Analysis of Dependency Quantified Boolean Formulas

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Preliminaries

2.1 DQBF and Its Subclasses

▶ Remark 1.

2.2 Manipulation of DQBFcnf

Lemma 2 (Universal reduction [3, 12]).

Lemma 3 (Variable elimination by resolution [20]).

2.3 Universal Expansion of 𝒌⁢-DQBF

3 Complexity of sat⁡(𝒌⁢-DQBFdnfd)

Theorem 4.

Corollary 5.

4 Complexity of sat⁡(𝒌⁢-DQBFcnf𝜶)

4.1 Universal Expansion of DQBFcnfd

Definition 6.

Lemma 7.

Proof.

4.2 𝟐⁢-DQBFcnfd

Theorem 8.

Definition 9 (Disimplex [11]).

Lemma 10.

Proof.

Proof of Theorem 8.

4.3 𝒌⁢-DQBFcnfd: 𝒌⩾𝟑 and Non-Constant 𝒌

Lemma 11.

Proof.

▶ Remark 12.

Lemma 13.

Proof.

Theorem 14.

Proof.

4.4 𝒌⁢-DQBFcnf𝜶: Different Dependency Structure

Theorem 15.

Proof.

Theorem 16.

Corollary 17.

Proof of Theorem 16.

Case 1: 𝑫𝒕=𝒙¯.

Case 2: 𝑫𝒕≠𝒙¯.

Lemma 18.

5 Complexity of sat⁡(𝒌⁢-DQBFcnf)

Theorem 19.

Proof.

Theorem 20.

Proof.

Theorem 21.

Proof.

Lemma 22 (Reformulated Tseitin Transformation).

Proof.

Theorem 23.

6 Conclusions and Future Work

References

Appendix A Additional Background

A.1 Tseitin Transformation

Appendix B Omitted Proofs

B.1 Complexity of sat⁡(𝒌⁢-DQBFdnfd)

Proof of Theorem 4.

B.2 Hardness of sat⁡(𝟑⁢-DQBFcnfd)

Hardness Proof of Theorem 14.

B.3 Proof of Lemma 18

Definition 24.

Lemma 25.

Proof.

Lemma 26.

Proof.

$\blacktriangleright$ Remark 1.

2.2 Manipulation of $\textup{DQBF}_{\textup{{cnf}}}$

2.3 Universal Expansion of $k\textup{-DQBF}$

3 Complexity of $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{dnf}}}^{\textup{{d}}})$

4 Complexity of $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{$% \alpha$}}})$

4.1 Universal Expansion of $\textup{DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$

4.2 $2\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$

4.3 $k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}}$ : $k\geqslant 3$ and Non-Constant $𝒌$

$\blacktriangleright$ Remark 12.

4.4 $k\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{$\alpha$}}}$ : Different Dependency Structure

Case 1: $D_{t}=\bar{x}$ .

Case 2: $D_{t}\neq\bar{x}$ .

5 Complexity of $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{cnf}}})$

B.1 Complexity of $\operatorname{\textup{{sat}}}(k\textup{-DQBF}_{\textup{{dnf}}}^{\textup{{d}}})$

B.2 Hardness of $\operatorname{\textup{{sat}}}(3\textup{-DQBF}_{\textup{{cnf}}}^{\textup{{d}}})$