DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL

TL;DR

DepQBF 6.0 introduces a generalized QRES-based QCDCL solver that can produce shorter proofs for QBFs, advancing the state of the art in QBF solving techniques.

Contribution

It presents a novel generalization of QRES within QCDCL, enabling potentially exponential proof size reductions compared to traditional methods.

Findings

Generalized QRES enables shorter proofs.

Experimental results show improved solver effectiveness.

DepQBF 6.0 outperforms previous versions.

Abstract

We present the latest major release version 6.0 of the quantified Boolean formula (QBF) solver DepQBF, which is based on QCDCL. QCDCL is an extension of the conflict-driven clause learning (CDCL) paradigm implemented in state of the art propositional satisfiability (SAT) solvers. The Q-resolution calculus (QRES) is a QBF proof system which underlies QCDCL. QCDCL solvers can produce QRES proofs of QBFs in prenex conjunctive normal form (PCNF) as a byproduct of the solving process. In contrast to traditional QCDCL based on QRES, DepQBF 6.0 implements a variant of QCDCL which is based on a generalization of QRES. This generalization is due to a set of additional axioms and leaves the original Q-resolution rules unchanged. The generalization of QRES enables QCDCL to potentially produce exponentially shorter proofs than the traditional variant. We present an overview of the features implemented in DepQBF and report on experimental results which demonstrate the effectiveness of generalized QRES in QCDCL.

Figures

Tables

Table 1. Table 1: Solved instances ( S ), solved unsatisfiable ( ⊥ bottom \bot ) and satisfiable ones ( ⊤ top \top ), uniquely solved ones among all solvers ( U ), and total wall clock time including time outs on 825 PCNFs from QBFEVAL’16 without ( 0a ) and with preprocessing by Bloqqer ( 0b ).

Solver	S	$\perp$	$\top$	U	Time
AIGSolve	603	301	302	34	440K
GhostQ	593	292	301	7	457K
QSTS	578	294	284	3	469K
DQ	458	255	203	0	682K
DQ-linldq	458	257	201	2	686K
DQ-lin	456	255	201	0	686K
DQ-ncl	448	246	202	0	703K
DQ-nq	397	228	169	0	788K
DQ-ncu	393	229	164	0	796K
DQ-n	383	221	162	0	814K
CAQE	378	202	176	9	831K
QESTO	369	210	159	0	864K
RAReQS	341	211	130	2	891K

Table 2. (a) Original instances.

Solver	S	$\perp$	$\top$	U	Time
AIGSolve	603	301	302	34	440K
GhostQ	593	292	301	7	457K
QSTS	578	294	284	3	469K
DQ	458	255	203	0	682K
DQ-linldq	458	257	201	2	686K
DQ-lin	456	255	201	0	686K
DQ-ncl	448	246	202	0	703K
DQ-nq	397	228	169	0	788K
DQ-ncu	393	229	164	0	796K
DQ-n	383	221	162	0	814K
CAQE	378	202	176	9	831K
QESTO	369	210	159	0	864K
RAReQS	341	211	130	2	891K

Table 3. (b) Preprocessed by Bloqqer .

Solver	S	$\perp$	$\top$	U	Time
QSTS	633	330	303	11	365K
RAReQS	633	334	299	8	375K
QESTO	620	321	299	0	395K
DQ-ncl	601	303	298	0	428K
DQ	601	301	300	0	429K
DQ-linldq	598	300	298	2	437K
DQ-lin	597	299	298	0	436K
CAQE	596	301	295	4	451K
DQ-n	593	296	297	0	444K
DQ-ncu	591	297	294	0	455K
DQ-nq	587	293	294	0	455K
GhostQ	570	282	288	0	485K
AIGSolve	567	286	281	14	481K

Table 4. Table 2: Related to Table  0a : solver performance on 402 filtered original ( not preprocessed ) instances partitioned into 261 instances with at most two ( 1a ) and 141 with three or more quantifier alternations ( 1b ).

Solver	S	$\perp$	$\top$	U	Time
GhostQ	176	75	101	5	171K
AIGSolve	138	66	72	14	250K
QSTS	136	58	78	0	232K
RAReQS	76	43	33	1	340K
DQ-lin	69	35	34	0	351K
DQ	69	35	34	0	351K
DQ-ncl	68	35	33	0	354K
DQ-linldq	67	34	33	0	354K
QESTO	66	37	29	0	359K
DQ-ncu	53	24	29	0	378K
DQ-n	52	24	28	0	378K
DQ-nq	52	23	29	0	379K
CAQE	43	17	26	3	397K

Table 5. (a) At most two quantifier alternations.

Solver	S	$\perp$	$\top$	U	Time
GhostQ	176	75	101	5	171K
AIGSolve	138	66	72	14	250K
QSTS	136	58	78	0	232K
RAReQS	76	43	33	1	340K
DQ-lin	69	35	34	0	351K
DQ	69	35	34	0	351K
DQ-ncl	68	35	33	0	354K
DQ-linldq	67	34	33	0	354K
QESTO	66	37	29	0	359K
DQ-ncu	53	24	29	0	378K
DQ-n	52	24	28	0	378K
DQ-nq	52	23	29	0	379K
CAQE	43	17	26	3	397K

Table 6. (b) Three or more quantifier alternations.

Solver	S	$\perp$	$\top$	U	Time
DQ-linldq	81	50	31	2	120K
DQ	79	47	32	0	119K
DQ-ncl	79	47	32	0	120K
DQ-lin	78	47	31	0	123K
QSTS	72	44	28	3	132K
DQ-nq	56	37	19	0	159K
GhostQ	56	31	25	2	160K
DQ-n	55	36	19	0	159K
DQ-ncu	55	36	19	0	159K
AIGSolve	54	25	29	9	161K
QESTO	49	33	16	0	179K
CAQE	46	29	17	2	182K
RAReQS	43	33	10	0	180K

Table 7. Table 3: Related to Table  0b : solver performance on 402 filtered and preprocessed instances partitioned into 270 instances with at most two ( 2a ) and 132 with three or more quantifier alternations ( 2b ).

Solver	S	$\perp$	$\top$	U	Time
RAReQS	157	79	78	8	227K
QESTO	138	66	72	0	255K
QSTS	136	62	74	2	255K
CAQE	118	49	69	2	298K
GhostQ	111	46	65	1	304K
DQ	107	43	64	1	311K
DQ-lin	106	42	64	0	311K
DQ-ncl	105	43	62	0	312K
DQ-n	105	41	64	0	313K
DQ-linldq	104	40	64	0	315K
AIGSolve	102	49	53	7	313K
DQ-nq	102	39	63	0	322K
DQ-ncu	102	40	62	0	323K

Table 8. (a) At most two quantifier alternations.

Solver	S	$\perp$	$\top$	U	Time
RAReQS	157	79	78	8	227K
QESTO	138	66	72	0	255K
QSTS	136	62	74	2	255K
CAQE	118	49	69	2	298K
GhostQ	111	46	65	1	304K
DQ	107	43	64	1	311K
DQ-lin	106	42	64	0	311K
DQ-ncl	105	43	62	0	312K
DQ-n	105	41	64	0	313K
DQ-linldq	104	40	64	0	315K
AIGSolve	102	49	53	7	313K
DQ-nq	102	39	63	0	322K
DQ-ncu	102	40	62	0	323K

Table 9. (b) Three or more quantifier alternations.

Solver	S	$\perp$	$\top$	U	Time
DQ-ncl	83	51	32	0	96K
DQ	81	49	32	0	98K
DQ-linldq	81	51	30	2	102K
DQ-lin	78	48	30	0	105K
DQ-ncu	76	48	28	0	112K
QSTS	75	50	25	1	107K
DQ-n	75	46	29	0	112K
DQ-nq	72	45	27	0	113K
QESTO	69	45	24	0	120K
CAQE	64	42	22	0	136K
RAReQS	62	45	17	1	131K
AIGSolve	51	27	24	6	151K
GhostQ	46	26	20	0	162K

Table 10. Table 4: Related to Table  0a (no preprocessing): the 825 PCNFs are partitioned into 466 PCNFs with at most two ( 3a ), and 359 PCNFs with three or more quantifier alternations ( 3b ).

Solver	S	$\perp$	$\top$	U	Time
AIGSolve	338	170	168	25	262K
GhostQ	336	160	176	5	257K
QSTS	292	143	149	0	325K
DQ-lin	233	126	107	0	429K
DQ	233	126	107	0	429K
DQ-linldq	231	125	106	0	431K
RAReQS	231	140	91	2	434K
DQ-ncl	223	117	106	0	449K
QESTO	213	126	87	0	474K
DQ-nq	202	110	92	0	483K
DQ-ncu	197	111	86	0	492K
DQ-n	188	103	85	0	509K
CAQE	174	91	83	4	535K

Table 11. (a) At most two quantifier alternations.

Solver	S	$\perp$	$\top$	U	Time
AIGSolve	338	170	168	25	262K
GhostQ	336	160	176	5	257K
QSTS	292	143	149	0	325K
DQ-lin	233	126	107	0	429K
DQ	233	126	107	0	429K
DQ-linldq	231	125	106	0	431K
RAReQS	231	140	91	2	434K
DQ-ncl	223	117	106	0	449K
QESTO	213	126	87	0	474K
DQ-nq	202	110	92	0	483K
DQ-ncu	197	111	86	0	492K
DQ-n	188	103	85	0	509K
CAQE	174	91	83	4	535K

Table 12. (b) Three or more quantifier alternations.

Solver	S	$\perp$	$\top$	U	Time
QSTS	286	151	135	3	144K
AIGSolve	265	131	134	9	177K
GhostQ	257	132	125	2	199K
DQ-linldq	227	132	95	2	254K
DQ	225	129	96	0	253K
DQ-ncl	225	129	96	0	254K
DQ-lin	223	129	94	0	257K
CAQE	204	111	93	5	295K
DQ-ncu	196	118	78	0	304K
DQ-n	195	118	77	0	304K
DQ-nq	195	118	77	0	305K
QESTO	156	84	72	0	390K
RAReQS	110	71	39	0	456K

Table 13. Table 5: Related to Table  0b (preprocessed by Bloqqer ): the 825 PCNFs are partitioned into 693 PCNFs with at most two ( 4a ), and 132 PCNFs with three or more quantifier alternations ( 4b ).

Solver	S	$\perp$	$\top$	U	Time
RAReQS	571	289	282	16	243K
QSTS	558	280	278	2	258K
QESTO	551	276	275	0	274K
CAQE	532	259	273	2	315K
GhostQ	524	256	268	1	323K
DQ	520	252	268	1	331K
DQ-lin	519	251	268	0	331K
DQ-n	518	250	268	0	332K
DQ-ncl	518	252	266	0	332K
DQ-linldq	517	249	268	0	334K
AIGSolve	516	259	257	7	329K
DQ-nq	515	248	267	0	342K
DQ-ncu	515	249	266	0	342K

Table 14. (a) At most two quantifier alternations.

Solver	S	$\perp$	$\top$	U	Time
RAReQS	571	289	282	16	243K
QSTS	558	280	278	2	258K
QESTO	551	276	275	0	274K
CAQE	532	259	273	2	315K
GhostQ	524	256	268	1	323K
DQ	520	252	268	1	331K
DQ-lin	519	251	268	0	331K
DQ-n	518	250	268	0	332K
DQ-ncl	518	252	266	0	332K
DQ-linldq	517	249	268	0	334K
AIGSolve	516	259	257	7	329K
DQ-nq	515	248	267	0	342K
DQ-ncu	515	249	266	0	342K

Table 15. (b) Three or more quantifier alternations.

Solver	S	$\perp$	$\top$	U	Time
DQ-ncl	83	51	32	0	96K
DQ	81	49	32	0	98K
DQ-linldq	81	51	30	2	102K
DQ-lin	78	48	30	0	105K
DQ-ncu	76	48	28	0	112K
QSTS	75	50	25	1	107K
DQ-n	75	46	29	0	112K
DQ-nq	72	45	27	0	113K
QESTO	69	45	24	0	120K
CAQE	64	42	22	0	136K
RAReQS	62	45	17	1	131K
AIGSolve	51	27	24	6	151K
GhostQ	46	26	20	0	162K

Equations

$$C\cup \{l\}$$

$$C$$

$$A$$

$$C_1\cup \{p\}$$

$$C\cup \{l\}$$

Full text

1 Introduction

Propositional satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) [43] implement a combination of the DPLL algorithm [11] and propositional resolution [40] to derive learned clauses from a CNF to be solved.

CDCL has been extended to solve quantified Boolean formulas (QBFs) [20], resulting in the QCDCL approach [14, 24, 48]. The logic of QBFs allows for explicit universal and existential quantification of propositional variables. As a consequence, the satisfiability problem of QBFs is PSPACE-complete.

In contrast to SAT solving, where CDCL is the dominant solving paradigm in practice, QCDCL is complemented by variable expansion [1, 6]. This approach successively eliminates variables from a QBF until it reduces to either true or false. Many modern solvers (e.g. [17, 19, 39]) implement expansion by counter-example guided abstraction refinement (CEGAR) [10].

The Q-resolution calculus (QRES) [14, 21, 24, 48] is a QBF proof system that underlies QCDCL in a way that is analogous to propositional resolution in CDCL. The empty clause is derivable from a PCNF $\psi$ by QRES iff $\psi$ is unsatisfiable. According to QBF proof complexity, there is an exponential separation between the sizes of proofs that variable expansion and Q-resolution can produce for certain QBFs [5, 18]. This theoretical result suggests to combine such orthogonal proof systems in QBF solvers to leverage their individual strengths.

As a first step towards a solver framework that allows for the combination of QBF proof systems in a systematic way, we present the latest major release version 6.0 of the QCDCL solver DepQBF.111DepQBF is licensed under GPLv3: http://lonsing.github.io/depqbf/ In contrast to traditional QCDCL based on QRES [14, 21, 24, 48], DepQBF 6.0 implements a variant of QCDCL that relies on a generalization of QRES. This generalization is due to a set of new axioms added to QRES [31]. In practice, derivations made by the added axioms in QCDCL are based on arbitrary QBF proof systems. As a consequence, when applying proof systems that are orthogonal to Q-resolution, the generalization of QRES via the new axioms enables QCDCL as implemented in DepQBF 6.0 to potentially produce exponentially shorter proofs than traditional QCDCL.

We report on experiments where we compare DepQBF 6.0 to state of the art QBF solvers. Experimental results demonstrate the effectiveness of generalized QRES in QCDCL. Additionally, we briefly summarize the evolution of DepQBF since the first version 0.1 [26]. We relate the features that were added to the different versions of DepQBF over time to the enhanced variant of QCDCL implemented in DepQBF 6.0.

2 Preliminaries

A QBF $\psi:=\Pi.\phi$ in prenex conjunctive normal form (PCNF) consists of a quantifier prefix $\Pi:=Q_{1}X_{1}\ldots Q_{n}X_{n}$ and a CNF $\phi$ not containing tautological clauses. The CNF $\phi$ is defined over the propositional variables $X_{1}\cup\ldots\cup X_{n}$ that appear in $\Pi$. The variable sets $X_{i}$ are pairwise disjoint and $Q_{i}\not=Q_{i+1}$ for $Q_{i}\in\{\forall,\exists\}$. QBFs $\psi:=\Pi.\phi$ in prenex disjunctive normal form (PDNF) are defined analogously to PCNFs, where $\phi$ is a DNF consisting of cubes. A cube is a conjunction of literals. The quantifier $\mathsf{Q}(\Pi,l)$ of a literal $l$ is $Q_{i}$ if the variable $\mathsf{var}(l)$ of $l$ appears in $X_{i}$. If $\mathsf{Q}(\Pi,l)=Q_{i}$ and $\mathsf{Q}(\Pi,k)=Q_{j}$, then $l\leq_{\Pi}k$ iff $i\leq j$.

An assignment $A$ maps variables of a QBF $\Pi.\phi$ to truth values true ($\top$) and false ($\bot$). We represent $A=\{l_{1},\ldots,l_{n}\}$ as a set of literals such that if a variable $x$ is assigned true (false) then $l_{i}\in A$ with $l_{i}=x$ ($l_{i}=\bar{x}$), where $\bar{x}$ is the negation of $x$. Further, $\mathsf{var}(l_{i})\not=\mathsf{var}(l_{j})$ for any $l_{i},l_{j}\in A$ with $i\not=j$.

The PCNF $\psi$ under assignment $A$, written as $\psi[A]$, is the PCNF obtained from $\psi$ in which for all $l\in A$, all clauses containing $l$ are removed, all occurrences of $\bar{l}$ are deleted, and $\mathsf{var}(l)$ is removed from the prefix. If the CNF of $\psi[A]$ is empty (respectively, contains the empty clause $\emptyset$), then it is satisfied (falsified) by $A$ and $A$ is a satisfying (falsifying) assignment, written as $\psi[A]=\top$ ($\psi[A]=\bot$). A PDNF $\psi$ under an assignment $A$ and an empty cube are defined in a way dual to PCNFs and empty clauses. A QBF $\Pi.\phi$ with $Q_{1}=\exists$ ($Q_{1}=\forall$) is satisfiable iff, for $x\in X_{1}$, $\Pi.\phi[\{x\}]$ or (and) $\Pi.\phi[\{\bar{x}\}]$ is satisfiable. Two QBFs $\psi$ and $\psi^{\prime}$ are satisfiability-equivalent ($\psi\equiv_{\mathit{sat}}\psi^{\prime}$), iff $\psi$ is satisfiable whenever $\psi^{\prime}$ is satisfiable.

3 QCDCL and the Generalized Q-Resolution Calculus

In the following, we present the variant of QCDCL implemented in DepQBF 6.0 that relies on a generalization of the Q-resolution calculus (QRES). We illustrate the workflow of that variant in Fig. 1.

In general, QCDCL is based on the successive generation of assignments that guide the application of the inference rules of QRES to derive learned clauses and cubes from a given input PCNF $\psi=\Pi.\phi$. Learned cubes are dual to clauses. While learned clauses represent assignments that falsify the CNF $\phi$ of $\psi$, learned cubes represent assignments that satisfy $\phi$. The empty cube is derivable from a PCNF $\psi$ by QRES iff $\psi$ is satisfiable. Based on our presentation of the rules of QRES we illustrate the differences between traditional QCDCL and the variant implemented in DepQBF 6.0.

A QCDCL solver maintains a PCNF $\theta=\Pi.\theta^{\prime}$ (PDNF $\gamma=\Pi.\gamma^{\prime}$) consisting of a CNF $\theta^{\prime}$ (DNF $\gamma^{\prime}$) of learned clauses (cubes). The clauses in $\theta$ are added conjunctively to $\psi$ to obtain $\psi_{\theta}=\Pi.(\phi\wedge(\bigwedge_{C\in\theta^{\prime}}C))$, and the cubes in $\gamma$ are added disjunctively to $\psi$ to obtain $\psi_{\gamma}=\Pi.(\phi\vee(\bigvee_{C\in\gamma^{\prime}}C))$. It holds that $\psi\equiv_{\mathit{sat}}\psi_{\theta}$ and $\psi\equiv_{\mathit{sat}}\psi_{\gamma}$. Initially the current assignment $A$, the PCNF $\theta$, and PDNF $\gamma$ are empty. We use the notation $C$, $C^{\prime}$, and $C_{L}$ for both clauses and cubes.

During propagation, the formulas $\psi_{\theta}$ and $\psi_{\gamma}$ are first simplified under the current assignment $A$ by computing $\psi_{\theta}[A]$ and $\psi_{\gamma}[A]$. Then universal and existential reduction is applied to $\psi_{\theta}[A]$ and to $\psi_{\gamma}[A]$ based on the following inference rule.

Definition 1 (Reduction [14, 21, 24, 48])

Let $\psi=\Pi.\phi$ be a PCNF.

[TABLE]

Universal (existential) reduction of clauses (cubes) by rule $\mathit{red}$ eliminates trailing universal (existential) literals from a clause (cube) with respect to the linear quantifier ordering in the prefix of the PCNF $\psi$. We write $\mathit{UR}(C)=C^{\prime}$ ($\mathit{ER}(C)=C^{\prime}$) to denote the clause (cube) $C^{\prime}$ resulting from clause (cube) $C$ by fully reducing universal (existential) literals.

Let $\psi_{\theta}^{\prime}$ and $\psi_{\gamma}^{\prime}$ denote the formulas obtained by applying universal (existential) reduction to all the clauses (cubes) in $\psi_{\theta}[A]$ ($\psi_{\gamma}[A]$) until saturation. New assignments are generated by unit literal detection with respect to $\psi_{\theta}^{\prime}$ and $\psi_{\gamma}^{\prime}$. If a PCNF (PDNF) $\psi$ contains a unit clause (cube) $C=(l)$, where $\mathsf{Q}(\Pi,l)=\exists$ ($\mathsf{Q}(\Pi,l)=\forall$), then literal $l$ is unit and $\psi\equiv_{\mathit{sat}}\psi[A^{\prime}]$ where $A^{\prime}=\{l\}$ ($A^{\prime}=\{\bar{l}\}$). Assignment $A$ is extended by assignments $A^{\prime}$ derived from unit clauses (cubes) in $\psi_{\theta}^{\prime}$ ($\psi_{\gamma}^{\prime}$). For every unit clause (cube) $C^{\prime}\in\psi_{\theta}^{\prime}$ ($C^{\prime}\in\psi_{\gamma}^{\prime}$) with $C^{\prime}=(l)$, the corresponding assignment $A^{\prime}:=\{l\}$ ($A^{\prime}:=\{\bar{l}\}$) is recorded.

After propagation, in conflict/solution detection it is checked whether $\psi_{\theta}^{\prime}$ is unsatisfiable or whether $\psi_{\gamma}^{\prime}$ is satisfiable (only one of the two cases can occur). To this end, incomplete methods are applied. In traditional QCDCL, for example, it is syntactically checked if the current assignment $A$ is falsifying or satisfying, i.e., whether $\psi_{\theta}^{\prime}$ contains the empty clause (i.e., $\psi_{\theta}^{\prime}=\bot$) or whether $\psi_{\gamma}^{\prime}$ contains the empty cube (i.e., $\psi_{\gamma}^{\prime}=\top$). In DepQBF 6.0, we extend these incomplete syntactic checks to incomplete semantic checks based on arbitrary QBF decision procedures (proof systems) that are applied to $\psi_{\theta}^{\prime}$ and $\psi_{\gamma}^{\prime}$ in a resource bounded way.

If neither $\psi_{\theta}^{\prime}$ is found unsatisfiable nor $\psi_{\gamma}^{\prime}$ is found satisfiable by the incomplete satisfiability checks, then in decision making $A$ is extended by heuristically assigning some decision variable $x$ from the leftmost quantifier block of $\psi[A]$ ($A:=A\cup\{l\}$ where $\mathsf{var}(l)=x$), and propagation continues. Assignments by decision making must follow the prefix ordering of $\psi$, in contrast to assignments by propagation (unit literals), which results in assignments of the following kind.

Definition 2 (QCDCL assignment [25])

Assignments generated by decision making and propagation in QCDCL are called QCDCL assignments.

If $\psi_{\theta}^{\prime}$ ($\psi_{\gamma}^{\prime}$) is found unsatisfiable (satisfiable) in conflict/solution detection then a learned clause (cube) is derived using QRES depending on the incomplete satisfiability checks. In traditional QCDCL, conflict/solution detection relies only on falsifying or satisfying assignments. If $\psi_{\theta}^{\prime}=\bot$ then $\psi_{\theta}^{\prime}$ contains an empty clause $C^{\prime}=\emptyset$ such that there is a clause $C\in\psi_{\theta}$ with $C^{\prime}=\mathit{UR}(C[A])$. Clause $C$ is the falsified clause with respect to assignment $A$. If $C$ appears in the given PCNF $\psi$ then in traditional QRES it is derived trivially by the following axiom.

Definition 3 (Clause Axiom [14, 21, 24, 48])

Let $\psi=\Pi.\phi$ be a PCNF.

[TABLE]

If $\psi_{\theta}^{\prime}\not=\bot$ but $\psi_{\gamma}^{\prime}=\top$ then either (1) $\psi_{\gamma}^{\prime}$ contains an empty learned cube $C^{\prime}=\emptyset$ such that there is a cube $C\in\psi_{\gamma}$ with $C^{\prime}=\mathit{ER}(C[A])$, or (2) $A$ is a satisfying assignment that satisfies all clauses in $\psi_{\gamma}^{\prime}$. For case (2), a cube $C$ is derived by the following axiom of traditional QRES (in either case (1) or (2) cube $C$ is the satisfied cube with respect to $A$).

Definition 4 (Cube Axiom [14, 21, 24, 48])

Let $\psi=\Pi.\phi$ be a PCNF.

[TABLE]

DepQBF 6.0 supports the application of arbitrary (incomplete) QBF decision procedures (proof systems) in conflict/solution detection and thus generalizes the syntactic checks for falsifying and satisfying assignments in traditional QCDCL.

To check the satisfiability of $\psi_{\gamma}^{\prime}$, in DepQBF 6.0 we apply a dynamic variant of blocked clause elimination (QBCE) [25]. This approach was introduced in version 5.0 of DepQBF. QBCE has been presented as a preprocessing technique to eliminate redundant blocked clauses [15, 23] from a PCNF. If all clauses in $\psi_{\gamma}^{\prime}$ are satisfied under $A$ or identified as blocked, then $\psi_{\gamma}^{\prime}$ is determined satisfiable. In our implementation applications of QBCE are tightly integrated in the propagation phase via efficient data structures. Clauses that are blocked are temporarily considered as removed from the formula. Hence such clauses cannot be used to detect unit clauses or empty clauses during propagation.

In addition to dynamic QBCE, we implemented incomplete QBF satisfiability checks based on propositional abstractions of $\psi_{\theta}^{\prime}$ and $\psi_{\gamma}^{\prime}$ [31], which are solved using an integrated SAT solver. These abstractions are constructed by treating universally quantified literals in the given PCNF $\psi$ in a special way. Propositional abstractions and SAT solving leverage the benefits of techniques like trivial truth and trivial falsity presented already in early search-based QBF solvers [9]. Additionally, the power of QU-resolution [47], which is exponentially stronger than Q-resolution [21] but has not been applied systematically in QCDCL, is harnessed to a certain extent (cf. Example 3 in [31]).

As a simple way of applying a QBF decision procedure that is incomplete by its nature we integrated the preprocessor Bloqqer [15] in DepQBF 6.0. Preprocessing aims at simplifying a formula within a restricted amount of time but might already solve certain formulas (cf. [33]). Among several techniques, Bloqqer applies bounded expansion of universally quantified variables [6, 8]. Hence by integrating Bloqqer in QCDCL we in fact integrate expansion, a QBF proof system that is orthogonal to Q-resolution [5, 18]. Due to usability issues, in the follow-up release version 6.02 of DepQBF we replaced Bloqqer by the expansion based QBF solver Nenofex,222https://github.com/lonsing/nenofex which is applied in a resource bounded way.

If $\psi_{\theta}^{\prime}$ ($\psi_{\gamma}^{\prime}$) is found unsatisfiable (satisfiable) by an incomplete decision procedure but, unlike above, $A$ is neither falsifying nor satisfying, then a clause (cube) is derived by the following generalized axioms of QRES. These axioms are added to QRES and applied in addition to the traditional axioms $\operatorname{\emph{cl-init}}$ and $\operatorname{\emph{cu-init}}$.

Definition 5 (Generalized Axioms [31])

Let $\psi=\Pi.\phi$ be a PCNF.

[TABLE]

[TABLE]

Note that the generalized axioms allow to derive clauses and cubes that cannot be derived by the traditional axioms $\operatorname{\emph{cl-init}}$ and $\operatorname{\emph{cu-init}}$ in general. This is due to the application of arbitrary QBF decision procedures (proof systems) for satisfiability checking in conflict/solution detection or in the side conditions of the axioms, respectively. In the side conditions the satisfiability of the PCNF $\psi[A]$ is checked, in contrast to formulas $\psi_{\theta}^{\prime}$ and $\psi_{\gamma}^{\prime}$ as in conflict/solution detection. This is possible since $\psi_{\theta}^{\prime}\equiv_{\mathit{sat}}\psi[A]$ and $\psi_{\gamma}^{\prime}\equiv_{\mathit{sat}}\psi[A]$. The clause (cube) $C$ derived by applying the generalized clause axiom $\operatorname{\emph{gen-cl-init}}$ ($\operatorname{\emph{gen-cu-init}}$) is the falsified clause (satisfied cube) with respect to $A$.

During clause (cube) learning, a new learned clause (cube) $C_{L}$ is derived by QRES. The falsified clause (satisfied cube) $C$ is the start clause (cube) of a derivation of $C_{L}$. Given $A$, clauses (cubes) which became unit during propagation are systematically resolved based on the following Q-resolution rule.

Definition 6 (Q-Resolution [21])

Let $\psi=\Pi.\phi$ be a PCNF.

[TABLE]

Rule $\mathit{res}$ does not allow the resolvent $(C_{1}\cup C_{2})$ to be a tautological clause (contradictory cube) and requires existential (universal) variables as pivots $p$. In general, learning produces a nonempty clause (cube) $C_{L}\not=\emptyset$, which is added to the PCNF $\theta$ (PDNF $\gamma$) of learned clauses (cubes), and hence also to $\psi_{\theta}$ ($\psi_{\gamma}$).

In backtracking, a certain subassignment $A^{\prime}\subset A$ is retracted such that $C_{L}$ becomes unit in propagation. $C_{L}$ is called an asserting clause (cube) [14]. Clauses (cubes) derived by rules $\operatorname{\emph{cl-init}}$ and $\operatorname{\emph{gen-cl-init}}$ ($\operatorname{\emph{cu-init}}$ and $\operatorname{\emph{gen-cu-init}}$) are used in exactly the same way in learning to produce asserting clauses (cubes).

QCDCL terminates (“UNSAT” or “SAT” in Fig. 1) by deriving the empty learned clause (cube) $C_{L}=\emptyset$. A clause (cube) resolution proof of the unsatisfiability (satisfiability) of $\psi$ can be obtained from the derivations of the learned clauses (cubes) up to the empty clause (cube).

By applying the generalized axioms using a complete QBF decision procedure, the empty assignment $A$, and an unlimited amount of time, the empty clause (cube) can be derived right away from any given unsatisfiable (satisfiable) PCNF $\psi$. In practice it is crucial to apply incomplete polynomial time procedures to limit the time spent on the satisfiability checks. However, the costs of frequent checks may outweigh the benefits. Hence in DepQBF 6.0, satisfiability checks for applications of the generalized axioms are dynamically disabled if they turn out to be too costly, and the traditional axioms are used instead. We refer to related work for implementation details [25, 31].

4 Features of DepQBF

We briefly summarize the general features of DepQBF that have been incorporated since its initial version 0.1 [26, 27]. Most features were described in related publications. Additionally, we comment on the compatibility of the features with the implementation of QRES with generalized axioms (Fig. 1) in DepQBF 6.0.

Dependency Schemes.

Since the initial version 0.1, DepQBF has been equipped with the standard dependency scheme [41] to relax the linear quantifier ordering in the prefix of a given PCNF $\psi$. In general, dependency schemes are used to compute dependency relations $D$, which are binary relations over the set of variables in $\psi$. If $(x,y)\not\in D$ for two variables $x$ and $y$ then the ordering of $x$ and $y$ in $\psi$ can safely be swapped. Otherwise, if $(x,y)\in D$ then $y$ is considered to depend on $x$. The integration of dependency schemes in QCDCL results in the following reduction rule, which is added to QRES and implemented in DepQBF.

Definition 7 (Dependency-Aware Reduction [27])

Let $\psi=\Pi.\phi$ be a PCNF and $D$ be a dependency relation computed using a dependency scheme.

[TABLE]

Rule $\operatorname{\emph{dep-red}}$ generalizes the traditional reduction rule $\mathit{red}$ by the use of dependency relation instead of the linear ordering of variables ($\leq_{\Pi}$) in the prefix of PCNF $\psi$. This way, it might be possible to reduce literals by rule $\operatorname{\emph{dep-red}}$ which cannot be reduced by rule $\mathit{red}$. The soundness of QRES with rule $\operatorname{\emph{dep-red}}$ has been proved for a dependency relation that is even more general (and thus allows for additional reductions) than the one implemented in DepQBF [44, 45, 46]. The generalized axioms $\operatorname{\emph{gen-cl-init}}$ and $\operatorname{\emph{gen-cu-init}}$ of QRES implemented in DepQBF 6.0 are naturally compatible with rule $\operatorname{\emph{dep-red}}$. Additionally, dependency schemes enable a relaxed variant of QCDCL assignments (Definition 2) based on the respective dependency relation rather than the prefix ordering of a PCNF $\psi$.

Long-Distance Resolution.

The Q-resolution rule $\mathit{res}$ [21] explicitly disallows to generate clauses (cubes) that are tautological (contradictory). This restriction is relaxed under certain side conditions in long-distance (LD) Q-resolution [2, 48, 49]. LDQ-resolution was first implemented in the QCDCL solver Quaffle [48] and was incorporated in version 3.0 of DepQBF. Compared to QRES with traditional Q-resolution $\mathit{res}$ [21], QRES with LDQ-resolution is exponentially more powerful in terms of proof sizes [13]. The generalized axioms $\operatorname{\emph{gen-cl-init}}$ and $\operatorname{\emph{gen-cu-init}}$ implemented in DepQBF 6.0 are not only compatible with the LDQ-resolution rule, but with any variants of Q-resolution (cf. [3]). Recently, the soundness of the combination of LDQ-resolution of clauses and dependency schemes in QRES has been proved [4, 37], leaving the soundness of cube resolutions as an open problem. Therefore, the combination of LDQ-resolution and dependency schemes is not supported in DepQBF 6.0.

Incremental Solving.

Since version 3.0, DepQBF has been equipped with an API in C and Java for incremental solving of sequences $S:=\langle\psi_{0},\ldots,\psi_{n}\rangle$ of syntactically related PCNFs $\psi_{i}$ [28, 34]. Incremental solving aims at reusing the clauses and cubes that were learned when solving PCNF $\psi_{i}$ when it comes to solve the PCNFs $\psi_{j}$ with $i<j$. The API of DepQBF allows to modify the PCNFs in $S$ by manipulating the quantifier prefix and adding or removing sets of clauses in a stack-based way. Since version 4.0, it is possible to add or remove sets of clauses arbitrarily [29] and to extract unsatisfiable cores, i.e., unsatisfiable subformulas of the PCNF $\psi_{i}$. At any time when solving $\psi_{i}\in S$, the soundness property of QCDCL (Section 3) that $\psi\equiv_{\mathit{sat}}\psi_{\theta}$ and $\psi\equiv_{\mathit{sat}}\psi_{\gamma}$, where $\psi=\psi_{i}$, must hold. To guarantee that property when using the generalized axioms for incremental solving, DepQBF 6.0 currently only applies the generalized cube axiom $\operatorname{\emph{gen-cu-init}}$ with dynamic QBCE used to check satisfiability of $\psi_{\gamma}^{\prime}$ in conflict/solution detection (Fig. 1). Although this configuration restricts the power of the generalized axioms, it has improved incremental solving in the context of QBF-based conformant planning [12]. As it is unclear how to use dependency schemes effectively in incremental solving, their application is disabled in DepQBF 6.0.

Generation of Proofs and Certificates.

QCDCL solvers can produce clause (cube) resolution proofs of the unsatisfiability (satisfiability) of PCNFs as a byproduct of clause (cube) learning. Since version 1.0 [36], DepQBF is capable of producing proofs without employing dependency schemes by rule $\operatorname{\emph{dep-red}}$. Given a proof $P$ of a PCNF $\psi$, a certificate of $\psi$ can be extracted from $P$ by inspecting the reduction steps by rule $\mathit{red}$ in $P$ [2]. A certificate of an unsatisfiable (satisfiable) PCNF $\psi$ is given by a set of Herbrand (Skolem) functions which represent the universal (existential) variables in $\psi$. Applications of the generalized axioms in QCDCL in general impose considerable restrictions on the certificate extraction process. The workflow [2] to extract a certificate from $P$ was originally presented for traditional QRES proofs. If proof $P$ contains clauses (cubes) derived by rule $\operatorname{\emph{gen-cl-init}}$ (rule $\operatorname{\emph{gen-cu-init}}$), then $P$ may lack information needed to extract correct certificates. As a result, DepQBF 6.0 does not support cube resolution proof generation combined with the generalized cube axiom $\operatorname{\emph{gen-cu-init}}$. However, it supports clause resolution proof generation with the generalized clause axiom $\operatorname{\emph{gen-cl-init}}$ provided that only propositional abstractions and SAT solving are used for satisfiability checking in the side condition of this axiom.

Advanced Generation of Learned Clauses and Cubes.

The derivation of a single asserting clause (cube) starting from a falsified clause (satisfied cube) as implemented in traditional QCDCL [14, 24, 48] has an exponential worst case [47]. Since version 2.0 DepQBF comes with an approach that avoids this exponential case [32] by a revised selection of clauses (cubes) to be resolved in learning. This advanced approach is compatible with all the techniques presented above.

5 Experiments

We compare variants of DepQBF 6.02, which is the latest follow-up release of DepQBF 6.0, to top performing solvers of QBFEVAL’16 [38]. As benchmarks we consider all 825 instances from the PCNF track, both in original form (Table 0a) and preprocessed by Bloqqer version 37 (Table 0b). We take preprocessing into account as it might have a positive impact on certain solvers while a negative on others (cf. [33, 35]). Experiments were run on an AMD Opteron 6238 processor (2.6 GHz) under 64-bit Ubuntu Linux 12.04 with time and memory limits of 1800 seconds and seven GB. Exceeding the memory limit is counted as a time out.333We refer to the appendix of this paper with additional experimental results.

To assess the impact of the generalized axioms $\operatorname{\emph{gen-cl-init}}$ and $\operatorname{\emph{gen-cu-init}}$ on the performance, we consider DepQBF 6.02 using both $\operatorname{\emph{gen-cl-init}}$ and $\operatorname{\emph{gen-cu-init}}$ (variant DQ in the tables), without $\operatorname{\emph{gen-cl-init}}$ (DQ-ncl), without $\operatorname{\emph{gen-cu-init}}$ (DQ-ncu), and using no generalized axioms at all (DQ-n).

On original instances (Table 0a), DQ outperforms variants DQ-ncl, DQ-ncu, and DQ-n with restricted or without generalized axioms, respectively. Variant DQ-ncl without axiom $\operatorname{\emph{gen-cl-init}}$ outperforms variant DQ-ncu without $\operatorname{\emph{gen-cu-init}}$. We attribute this effect to the use of dynamic QBCE (among other techniques) for applications of the cube axiom $\operatorname{\emph{gen-cu-init}}$ in DQ-ncl. Compared to DQ, disabling only dynamic QBCE in variant DQ-nq severely impacts performance.

On preprocessed instances (Table 0b), we make similar observations regarding the impact of the generalized axioms like in Table 0a. However, variant DQ-ncl without the clause axiom $\operatorname{\emph{gen-cl-init}}$ is on par with DQ. Preprocessing may blur the structure of an instance. We conjecture that this blurring hinders the success of the QBF decision procedures in DepQBF, on which applications of the generalized axioms are based. In general the performance difference between the variants of DepQBF is smaller than on original instances. The rankings of the solvers RAReQS [17], QESTO [19], and CAQE [39] are improved substantially by preprocessing, whereas those of AIGSolve [42] and GhostQ [17, 22] become worse. The best variant DQ-ncl in Table 0b ranks fourth behind QSTS [7], RAReQS, and QESTO. However, the lag to the solver ranked third is 19 instances compared to 120 instances for the best variant DQ in Table 0a that also ranks fourth.

To analyze the effects of preprocessing in more detail, we filtered the 825 PCNFs from QBFEVAL’16 by discarding 354 PCNFs that are already solved by Bloqqer and 69 PCNFs where Bloqqer eliminated all universally quantified variables, resulting in a set of 402 PCNFs. Further, we considered the 402 PCNFs in their original form and preprocessed by Bloqqer and partitioned them into subsets containing PCNFs with at most two and with three or more quantifier alternations. Such partitioning is motivated by a related experimental study [30] where a large diversity of solver performance was observed on instance classes defined by alternations. Tables 2 and 3 show solver performance on these subsets without and with preprocessing, respectively. Notably, variants of DepQBF outperform the other solvers on the subsets with three or more alternations, both without and with preprocessing (Tables 1b and 2b).

All variants of DepQBF reported above apply dependency-aware reduction by rule $\operatorname{\emph{dep-red}}$. Variant DQ-lin is the same as DQ (including generalized axioms) but uses the traditional reduction rule $\mathit{red}$ based on the linear quantifier ordering of PCNFs. Variant DQ outperforms DQ-lin in all tables except Table 1a, where DQ-lin is on par, which illustrates the benefits of dependency schemes in QCDCL. Variant DQ-linldq differs from DQ-lin in the use of LDQ-resolution in learning instead of traditional Q-resolution by rule $\mathit{res}$. The results with LDQ-resolution are mixed, despite being a stronger proof system than Q-resolution. Variant DQ-linldq outperforms DQ-lin in all tables except Tables 1a and 2a, i.e., on instances with at most two quantifier alternations.

6 Conclusion

We presented the latest major release version 6.0 of the QCDCL solver DepQBF. DepQBF 6.0 implements a variant of QCDCL that is based on a generalization of the Q-resolution calculus (QRES). The generalization is achieved by equipping QRES with generalized clause and cube axioms to be used in clause and cube learning [31]. The generalized axioms provide an extensible framework of interfaces for the integration of arbitrary QBF proof systems in QRES, and hence in QCDCL. The integration of proof systems orthogonal to Q-resolution, such as variable expansion, enables QCDCL to potentially produce proofs that are exponentially shorter than proofs produced by traditional QCDCL. This way, the state of the art of QCDCL solving can be further advanced. A related open problem is the inability of plain QCDCL to exploit the full power of Q-resolution [16].

The workflow of QCDCL with generalized axioms is not tailored towards DepQBF 6.0 but can be implemented in any QCDCL solver. Furthermore, it is compatible with dependency schemes [41, 45] and any Q-resolution variant [3], which offers potential for further improvements.

Experiments with variants of DepQBF 6.0 showed considerable performance gains due to the application of generalized axioms. However, frequent applications are hindered by computationally expensive QBF satisfiability checks in the side conditions of the axioms. To limit the checking overhead, axiom applications must be carefully scheduled. In this respect, there is room for improvements in fine tuning DepQBF 6.0. Further, it may be beneficial to integrate the QBF decision procedures that are applied to satisfiability checking more tightly in the QCDCL workflow, like with dynamic blocked clause elimination (QBCE) [25].

Appendix 0.A Additional Experimental Data