${\textsf {QRAT}}^{+}$: Generalizing QRAT by a More Powerful QBF Redundancy Property

Abstract

The $\mathsf {QRAT}$ (quantified resolution asymmetric tautology) proof system simulates virtually all inference rules applied in state of the art quantified Boolean formula (QBF) reasoning tools. It consists of rules to rewrite a QBF by adding and deleting clauses and universal literals that have a certain redundancy property. To check for this redundancy property in $\mathsf {QRAT}$, propositional unit propagation (UP) is applied to the quantifier free, i.e., propositional part of the QBF. We generalize the redundancy property in the $\mathsf {QRAT}$ system by QBF specific UP (QUP). QUP extends UP by the universal reduction operation to eliminate universal literals from clauses. We apply QUP to an abstraction of the QBF where certain universal quantifiers are converted into existential ones. This way, we obtain a generalization of $\mathsf {QRAT}$ we call $\mathsf {QRAT}^{+}$. The redundancy property in $\mathsf {QRAT}^{+}$ based on QUP is more powerful than the one in $\mathsf {QRAT}$ based on UP. We report on proof theoretical improvements and experimental results to illustrate the benefits of $\mathsf {QRAT}^{+}$ for QBF preprocessing.

Supported by the Austrian Science Fund (FWF) under grant S11409-N23.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

In practical applications of propositional logic satisfiability (SAT), it is necessary to establish correctness guarantees on the results produced by SAT solvers by proof checking [7]. The DRAT (deletion resolution asymmetric tautology) [23] approach has become state of the art to generate and check propositional proofs.

The logic of quantified Boolean formulas (QBF) extends propositional logic by existential and universal quantification of the propositional variables. Despite the PSPACE-completeness of QBF satisfiability checking, QBF technology is relevant in practice due to the potential succinctness of QBF encodings [4].

DRAT has been lifted to QBF to obtain the $\mathsf {QRAT}$ (quantified RAT) proof system [8, 10]. $\mathsf {QRAT}$ allows to represent and check (un)satisfiability proofs of QBFs and compute Skolem function certificates of satisfiable QBFs. The $\mathsf {QRAT}$ system simulates virtually all inference rules applied in state of the art QBF reasoning tools, such as Q-resolution [15] including its variant long-distance Q-resolution [13, 25], and expansion of universal variables [3].

A $\mathsf {QRAT}$ proof of a QBF in prenex CNF consists of a sequence of inference steps that rewrite the QBF by adding and deleting clauses and universal literals that have the $\mathsf {QRAT}$ redundancy property. Informally, checking whether a clause C has $\mathsf {QRAT}$ amounts to checking whether all possible resolvents of C on a literal $l \in C$ (under certain restrictions) are propositionally implied by the quantifier-free CNF part of the QBF. The principle of redundancy checking by inspecting resolvents originates from the RAT property in propositional logic [12] and was generalized to first-order logic in terms of implication modulo resolution [14]. Instead of a complete (and thus computationally hard) propositional implication check on a resolvent, the $\mathsf {QRAT}$ system relies on an incomplete check by propositional unit propagation (UP). Thereby, it is checked whether UP can derive the empty clause from the CNF augmented by the negated resolvent. Hence redundancy checking in $\mathsf {QRAT}$ is unaware of the quantifier structure, which is entirely ignored in UP.

We generalize redundancy checking in $\mathsf {QRAT}$ by making it aware of the quantifier structure of a QBF. To this end, we check the redundancy of resolvents based on QBF specific UP (QUP). It extends UP by the universal reduction (UR) operation [15] and is a polynomial-time procedure like UP. UR is central in resolution based QBF calculi [1, 15] as it shortens individual clauses by eliminating universal literals depending on the quantifier structure. We apply QUP to abstractions of the QBF where certain universal quantifiers are converted into existential ones. The purpose of abstractions is that if a resolvent is found redundant by QUP on the abstraction, then it is also redundant in the original QBF.

Our contributions are as follows: (1) by applying QUP and QBF abstractions instead of UP, we obtain a generalization of the $\mathsf {QRAT}$ system which we call $\mathsf {QRAT}^{+}$. In contrast to $\mathsf {QRAT}$, redundancy checking in $\mathsf {QRAT}^{+}$ is aware of the quantifier structure of a QBF. We show that (2) the redundancy property in $\mathsf {QRAT}^{+}$ based on QUP is more powerful than the one in $\mathsf {QRAT}$ based on UP. $\mathsf {QRAT}^{+}$ can detect redundancies which $\mathsf {QRAT}$ cannot. As a formal foundation, we introduce (3) a theory of QBF abstractions used in $\mathsf {QRAT}^{+}$. Redundancy elimination by $\mathsf {QRAT}^{+}$ or $\mathsf {QRAT}$ can lead to (4) exponentially shorter proofs in certain resolution based QBF calculi, which we point out by a concrete example. Note that here we do not study the power of $\mathsf {QRAT}$ or $\mathsf {QRAT}^{+}$ as proof systems themselves, but the impact of redundancy elimination. Finally, we report on experimental results (5) to illustrate the benefits of redundancy elimination by $\mathsf {QRAT}^{+}$ and $\mathsf {QRAT}$ for QBF preprocessing. Our implementation of $\mathsf {QRAT}^{+}$ and $\mathsf {QRAT}$ for preprocessing is the first one reported in the literature.

2 Preliminaries

We consider QBFs $\phi \, {{:=}}\,\varPi .\psi$ in prenex conjunctive normal form (PCNF) with a quantifier prefix $\varPi \,{{:=}}\,Q_1B_1 \ldots Q_nB_n$ and a quantifier free CNF $\psi$ not containing tautological clauses. The prefix consists of quantifier blocks $Q_iB_i$, where $B_i$ are blocks (i.e., sets) of propositional variables and $Q_i \in \{\forall , \exists \}$ are quantifiers. We have $B_i \cap B_j = \emptyset$, $Q_i \not = Q_{i+1}$ and $Q_n = \exists$. The CNF $\psi$ is defined precisely over the variables $vars (\phi ) = vars (\psi )\,{{:=}}\,B_1 \cup \ldots \cup B_n$ in $\varPi$ so that all variables are quantified, i.e., $\phi$ is closed. The quantifier $\mathsf {Q}(\varPi ,l)$ of literal l is $Q_i$ if the variable $\mathsf {var}(l)$ of l appears in $B_i$. The set of variables in a clause C is $vars (C)\,{{:=}}\,\{x \mid l \in C, \mathsf {var}(l) = x\}$. A literal l is existential if $\mathsf {Q}(\varPi ,l) = \exists$ and universal if $\mathsf {Q}(\varPi ,l) = \forall$. If $\mathsf {Q}(\varPi ,l) = Q_i$ and $\mathsf {Q}(\varPi ,k) = Q_j$, then $l \le _\varPi k$ iff $i \le j$. We extend the ordering $\le _{\varPi }$ to an arbitrary but fixed ordering on the variables in every block $B_i$.

An assignment $\tau : vars (\phi ) \rightarrow \{\top , \bot \}$ maps the variables of a QBF $\phi$ to truth constants $\top$ (true) or $\bot$ (false). Assignment $\tau$ is complete if it assigns every variable in $\phi$, otherwise $\tau$ is partial. By $\tau (\phi )$ we denote $\phi$under $\tau$, where each occurrence of variable x in $\phi$ is replaced by $\tau (x)$ and x is removed from the prefix of $\phi$, followed by propositional simplifications on $\tau (\phi )$. We consider $\tau$ as a set of literals such that, for some variable x, $x \in \tau$ if $\tau (x) = \top$ and $\bar{x} \in \tau$ if $\tau (x) = \bot$.

An assignment tree [10] T of a QBF $\phi$ is a complete binary tree of depth $| vars (\phi )| + 1$ where the internal (non-leaf) nodes of each level are associated with a variable of $\phi$. An internal node is universal (existential) if it is associated with a universal (existential) variable. The order of variables along every path in T respects the extended order $\le _\varPi$ of the prefix $\varPi$ of $\phi$. An internal node associated with variable x has two outgoing edges pointing to its children: one labelled with $\bar{x}$ and another one labelled with x, denoting the assignment of x to false and true, respectively. Each path $\tau$ in T from the root to an internal node (leaf) represents a partial (complete) assignment. A leaf at the end of $\tau$ is labelled by $\tau (\phi )$, i.e., the value of $\phi$ under $\tau$. An internal node associated with an existential (universal) variable is labelled with $\top$ iff one (both) of its children is (are) labelled with $\top$. The QBF $\phi$ is satisfiable (unsatisfiable) iff the root of T is labelled with $\top$ ($\bot$).

Given a QBF $\phi$ and its assignment tree T, a subtree $T'$ of T is a pre-model [10] of $\phi$ if (1) the root of T is the root of $T'$, (2) for every universal node in $T'$ both children are in $T'$, and (3) for every existential node in $T'$ exactly one of its children is in $T'$. A pre-model $T'$ of $\phi$ is a model [10] of $\phi$, denoted by $T' \models _{t} \phi$, if each node in $T'$ is labelled with $\top$. A QBF $\phi$ is satisfiable iff it has a model. Given a QBF $\phi$ and one of its models $T'$, $T''$ is a rooted subtree of $T'$ ($T'' \subseteq T'$) if $T''$ has the same root as $T'$ and the leaves of $T''$ are a subset of the leaves of $T'$.

We consider CNFs $\psi$ defined over a set B of variables without an explicit quantifier prefix. A model of a CNF $\psi$ is a model $\tau$ of the QBF $\exists B. \psi$ which consists only of the single path $\tau$. We write $\tau \models \psi$ if $\tau$ is a model of $\psi$. For CNFs $\psi$ and $\psi '$, $\psi '$ is implied by $\psi$ ($\psi \models \psi '$) if, for all $\tau$, it holds that if $\tau \models \psi$ then $\tau \models \psi '$. Two CNFs $\psi$ and $\psi '$ are equivalent ($\psi \equiv \psi '$), iff $\psi \models \psi '$ and $\psi ' \models \psi$. We define notation to explicitly refer to QBF models. For QBFs $\phi$ and $\phi '$, $\phi '$ is implied by $\phi$ ($\phi \models _{t} \phi '$) if, for all T, it holds that if $T \models _{t} \phi$ then $T \models _{t} \phi '$. QBFs $\phi$ and $\phi '$ are equivalent ($\phi \equiv _{ t }\phi '$) iff $\phi \models _{t} \phi '$ and $\phi ' \models _{t} \phi$, and satisfiability equivalent ($\phi \equiv _{ sat }\phi '$) iff $\phi$ is satisfiable whenever $\phi '$ is satisfiable. Satisfiability equivalence of CNFs is defined analogously and denoted by the same symbol ‘$\equiv _{ sat }$’.

3 The Original $\mathsf {QRAT}$ Proof System

Before we generalize $\mathsf {QRAT}$, we recapitulate the original proof system [10] and emphasize that redundancy checking in $\mathsf {QRAT}$ is unaware of quantifier structures.

Definition 1

([10]). The outer clause of clause C on literal $l \in C$ with respect to prefix $\varPi$ is the clause $\mathsf {OC} (\varPi , C, l) \,{{:=}}\, \{ k \mid k \in C, k \le _\varPi l, k \not = l\}$.

The outer clause $\mathsf {OC} (\varPi , C, l) \subset C$ of C on $l \in C$ contains only literals that are smaller than or equal to l in the variable ordering of prefix $\varPi$, excluding l.

Definition 2

([10]). Let C be a clause with $l \in C$ and D be a clause with $\bar{l} \in D$ occurring in QBF $\varPi . \psi$. The outer resolvent of C with D on l with respect to $\varPi$ is the clause $\mathsf {OR} (\varPi , C, D, l) \,{{:=}}\, (C \setminus \{l\}) \cup \mathsf {OC} (\varPi , D, \bar{l})$.

Example 1

Given $\phi \,{{:=}}\, \exists x_1 \forall u \exists x_2. (C \wedge D)$ with $C \,{{:=}}\, (x_1 \vee u \vee x_2)$ and $D \,{{:=}}\, (\bar{x}_1 \vee \bar{u} \vee \bar{x}_2)$, we have $\mathsf {OR} (\varPi , C, D, x_1) = ( u \vee x_2)$, $\mathsf {OR} (\varPi , C, D, u) = ( x_1 \vee \bar{x}_1 \vee x_2)$, $\mathsf {OR} (\varPi , C, D, x_2) = ( x_1 \vee u \vee \bar{x}_1 \vee \bar{u})$, and $\mathsf {OR} (\varPi , D, C, \bar{u}) = ( x_1 \vee \bar{x}_1 \vee \bar{x}_2)$. Computing outer resolvents is asymmetric since $\mathsf {OR} (\varPi , C, D, u) \not = \mathsf {OR} (\varPi , D, C, \bar{u})$.

Definition 3

([10]). Clause C has property $\mathsf {QIOR}$ (quantified implied outer resolvent) on literal $l \in C$ with respect to QBF $\varPi . \psi$ iff $\psi \models \mathsf {OR} (\varPi , C, D, l)$ for all $D \in \psi$ with $\bar{l} \in D$.

Property $\mathsf {QIOR}$ relies on checking whether every possible outer resolvent $\mathsf {OR}$ of some clause C on a literal is redundant by checking if $\mathsf {OR}$ is propositionally implied by the quantifier-free CNF $\psi$ of the given QBF $\varPi . \psi$. If C has $\mathsf {QIOR}$ on literal $l \in C$ then, depending on whether l is existential or universal and side conditions, either C is redundant and can be removed from QBF $\varPi . \psi$ or l is redundant and can be removed from C, respectively, resulting in a satisfiability-equivalent QBF.

Theorem 1

([10]). Given a QBF $\phi \,{{:=}}\, \varPi . \psi$ and a clause $C \in \psi$ with $\mathsf {QIOR}$ on an existential literal $l \in C$ with respect to QBF $\phi ' \,{{:=}}\, \varPi . \psi '$ where $\psi ' \,{{:=}}\, \psi \setminus \{C\}$. Then $\phi \equiv _{ sat }\phi '$.

Theorem 2

([10]). Given a QBF $\phi _0 \,{{:=}}\, \varPi . \psi$ and $\phi \,{{:=}}\, \varPi . (\psi \cup \{C\})$ where C has $\mathsf {QIOR}$ on a universal literal $l \in C$ with respect to $\phi _0$. Let $\phi ' \,{{:=}}\, \varPi . (\psi \cup \{C'\})$ with $C' \,{{:=}}\, C \setminus \{l\}$. Then $\phi \equiv _{ sat }\phi '$.

Note that in Theorems 1 and 2 clause C is actually removed from the QBF for the check whether C has $\mathsf {QIOR}$ on a literal. Checking propositional implication ($\models$) as in Definition 3 is co-NP hard and hence intractable. Therefore, in practice a polynomial-time incomplete implication check based on propositional unit propagation (UP) is applied. The use of UP is central in the $\mathsf {QRAT}$ proof system.

Definition 4

(propositional unit propagation, UP). For a CNF $\psi$ and clause C, let $\psi \wedge \overline{C} \mathrel {\vdash _{^{_{1}}}} \emptyset$ denote the fact that propositional unit propagation (UP) applied to $\psi \wedge \overline{C}$ produces the empty clause, where $\overline{C}$ is the conjunction of the negation of all the literals in C. If $\psi \wedge \overline{C} \mathrel {\vdash _{^{_{1}}}} \emptyset$ then we write $\psi \mathrel {\vdash _{^{_{1}}}} C$ to denote that C can be derived from $\psi$ by UP (since $\psi \models C$).

Definition 5

([10]). Clause C has property $\mathsf {AT}$ (asymmetric tautology) with respect to a CNF $\psi$ iff $\psi \mathrel {\vdash _{^{_{1}}}} C$.

$\mathsf {AT}$ is a propositional clause redundancy property that is used in the $\mathsf {QRAT}$ proof system to check whether outer resolvents are redundant, thereby replacing propositional implication ($\models$) in Definition 3 by unit propagation ($\mathrel {\vdash _{^{_{1}}}}$) as follows.

Definition 6

([10]). Clause C has property $\mathsf {QRAT}$ (quantified resolution asymmetric tautology) on literal $l \in C$ with respect to QBF $\varPi . \psi$ iff, for all $D \in \psi$ with $\bar{l} \in D$, the outer resolvent $\mathsf {OR} (\varPi , C, D,l)$ has $\mathsf {AT}$ with respect to CNF $\psi$.

Example 2

Consider $\phi \,{{:=}}\, \exists x_1 \forall u \exists x_2. (C \wedge D)$ with $C \,{{:=}}\, (x_1 \vee u \vee x_2)$ and $D \,{{:=}}\, (\bar{x}_1 \vee \bar{u} \vee \bar{x}_2)$ from Example 1. C does not have $\mathsf {AT}$ with respect to CNF D, but C has $\mathsf {QRAT}$ on $x_2$ with respect to QBF $\exists x_1 \forall u \exists x_2. (D)$ since $\mathsf {OR} (\varPi , C, D, x_2) = ( x_1 \vee u \vee \bar{x}_1 \vee \bar{u})$ has $\mathsf {AT}$ with respect to CNF D.

$\mathsf {QRAT}$ is a restriction of $\mathsf {QIOR}$, i.e., a clause that has $\mathsf {QRAT}$ also has $\mathsf {QIOR}$ but not necessarily vice versa. Therefore, the soundness of removing redundant clauses and literals based on $\mathsf {QRAT}$ follows right from Theorems 1 and 2.

Based on the $\mathsf {QRAT}$ redundancy property, the $\mathsf {QRAT}$ proof system [10] consists of rewrite rules to eliminate redundant clauses, denoted by $\mathsf {QRATE}$, to add redundant clauses, denoted by $\mathsf {QRATA}$, and to eliminate redundant universal literals, denoted by $\mathsf {QRATU}$. In a $\mathsf {QRAT}$ satisfaction proof (refutation), a QBF is reduced to the empty formula (respectively, to a formula containing the empty clause) by applying the rewrite rules. The $\mathsf {QRAT}$ proof systems has an additional rule to eliminate universal literals by extended universal reduction ($\mathsf {EUR}$). We do not present $\mathsf {EUR}$ because it is not affected by our generalization of $\mathsf {QRAT}$, which we define in the following. Observe that $\mathsf {QIOR}$ and $\mathsf {AT}$ (and hence also $\mathsf {QRAT}$) are based on propositional implication ($\models$) and unit propagation ($\mathrel {\vdash _{^{_{1}}}}$), i.e., the quantifier structure of the given QBF is not exploited.

4 $\mathsf {QRAT}^{+}$: A More Powerful QBF Redundancy Property

We make redundancy checking of outer resolvents in $\mathsf {QRAT}$ aware of the quantifier structure of a QBF. To this end, we generalize $\mathsf {QIOR}$ and $\mathsf {AT}$ by replacing propositional implication ($\models$) and unit propagation ($\mathrel {\vdash _{^{_{1}}}}$) by QBF implication $(\models _{t})$ and QBF unit propagation, respectively. Thereby, we obtain a more general and more powerful notion of the $\mathsf {QRAT}$ redundancy property, which we call $\mathsf {QRAT}^{+}$.

First, in Proposition 2 we point out a property of $\mathsf {QIOR}$ (Definition 3) which is due to the following result from related work [21]: if we attach a quantifier prefix $\varPi$ to equivalent CNFs $\psi$ and $\psi '$, then the resulting QBFs are equivalent.

Proposition 1

([21]). Given CNFs $\psi$ and $\psi '$ such that $vars (\psi ) = vars (\psi ')$ and a quantifier prefix $\varPi$ defined precisely over $vars (\psi )$. If $\psi \equiv \psi '$ then $\varPi . \psi \equiv _{ t }\varPi . \psi '$.

Proposition 2

If clause C has $\mathsf {QIOR}$ on literal $l \in C$ with respect to QBF $\varPi . \psi$, then $\varPi . \psi \equiv _{ t }\varPi . (\psi \wedge \mathsf {OR} (\varPi , C, D, l))$ for all $D \in \psi$ with $\bar{l} \in D$.

Proof

Since C has $\mathsf {QIOR}$ on literal $l \in C$ with respect to QBF $\varPi . \psi$, by Definition 3 we have $\psi \models \mathsf {OR} (\varPi , C, D, l)$ for all $D \in \psi$ with $\bar{l} \in D$, and further also $\psi \equiv \psi \wedge \mathsf {OR} (\varPi , C, D, l)$. Then $\varPi . \psi \equiv _{ t }\varPi . (\psi \wedge \mathsf {OR} (\varPi , C, D, l))$ by Proposition 1.    $\square$

By Proposition 2 any outer resolvent $\mathsf {OR}$ of some clause C that has $\mathsf {QIOR}$ with respect to some QBF $\varPi . \psi$ is redundant in the sense that it can be added to the QBF $\varPi . \psi$ in an equivalence preserving way ($\equiv _{ t }$), i.e., $\mathsf {OR}$ is implied by the QBF $\varPi . \psi$ ($\models _{t}$). This is the central characteristic of our generalization $\mathsf {QRAT}^{+}$ of $\mathsf {QRAT}$. We develop a redundancy property used in $\mathsf {QRAT}^{+}$ which allows to, e.g., remove a clause C from a QBF $\varPi . \psi$ in a satisfiability preserving way (like in $\mathsf {QRAT}$, cf. Theorem 1.) if all respective outer resolvents of C are implied by the QBF $\varPi . (\psi \setminus \{C\})$. Since checking QBF implication is intractable just like checking propositional implication in $\mathsf {QIOR}$, in practice we apply a polynomial-time incomplete QBF implication check based on QBF unit propagation.

In the following, we develop a theoretical framework of abstractions of QBFs that underlies our generalization $\mathsf {QRAT}^{+}$ of $\mathsf {QRAT}$. Abstractions are crucial for the soundness of checking QBF implication by QBF unit propagation.

Definition 7

(nesting levels, prefix/QBF abstraction). Let $\phi \,{{:=}}\, \varPi . \psi$ be a QBF with prefix $\varPi \,{{:=}}\, Q_1B_1 \ldots Q_iB_i Q_{i+1}B_{i+1} \ldots Q_nB_n$. For a clause C, $levels (\varPi , C) \,{{:=}}\, \{i \mid \exists l \in C, \mathsf {Q}(\varPi ,l) = Q_i\}$ is the set of nesting levels in C.¹ The abstraction of $\varPi$ with respect to i with $0 \le i \le n$ produces the abstracted prefix $Abs (\varPi , i) \,{{:=}}\, \varPi$ for $i = 0$ and otherwise $Abs (\varPi , i) \,{{:=}}\, \exists (B_1 \cup \ldots \cup B_i) Q_{i+1}B_{i+1} \ldots Q_nB_n$. The abstraction of $\phi$ with respect to i with $0 \le i \le n$ produces the abstracted QBF $Abs (\phi , i) \,{{:=}}\, Abs (\varPi , i). \psi$ with prefix $Abs (\varPi , i)$.

Example 3

Given the QBF $\phi \,{{:=}}\, \varPi . \psi$ with prefix $\varPi \,{{:=}}\, \forall B_1 \exists B_2 \forall B_3 \exists B_4$. We have $Abs (\phi , 0) = \phi$, $Abs (\phi , 1) = Abs (\phi , 2) = \exists (B_1 \cup B_2) \forall B_3 \exists B_4. \psi$, $Abs (\phi , 3) = Abs (\phi , 4) = \exists (B_1 \cup B_2 \cup B_3 \cup B_4). \psi$.

In an abstracted QBF $Abs (\phi , i)$ universal variables from blocks smaller than or equal to $B_i$ are converted into existential ones. If the original QBF $\phi$ has a model T, then all nodes in T associated to universal variables must be labelled with $\top$, in particular the universal variables that are existential in $Abs (\phi , i)$. Hence, for all models T of $\phi$, every model $T^A$ of $Abs (\phi , i)$ is a subtree of T.

Proposition 3

Given a QBF $\phi \,{{:=}}\, \varPi . \psi$ with prefix $\varPi \,{{:=}}\, Q_1B_1 \ldots Q_iB_i \ldots Q_nB_n$ and $Abs (\phi , i)$ for some arbitrary i with $0 \le i \le n$. For all T and $T^A$ we have that if $T \models _{t} \phi$ and $T^A \subseteq T$ is a pre-model of $Abs (\phi ,i)$, then $T^{A} \models _{t} Abs (\phi ,i)$.

Proof

By induction on i. The base case $i \,{{:=}}\, 0$ is trivial.

As induction hypothesis (IH), assume that the claim holds for some i with $0 \le i < n$, i.e., for all T and $T^A$ we have that if $T \models _{t} \phi$ and $T^A \subseteq T$ is a pre-model of $Abs (\phi ,i)$, then $T^{A} \models _{t} Abs (\phi ,i)$. Consider $Abs (\phi , j)$ for $j = i+1$, which is an abstraction of $Abs (\phi , i)$. We have to show that, for all T and $T^B$ we have that if $T \models _{t} \phi$ and $T^B \subseteq T$ is a pre-model of $Abs (\phi ,j)$, then $T^{B} \models _{t} Abs (\phi ,j)$. We distinguish cases by the type of $Q_j$ in the abstracted prefix $Abs (\varPi , i) = \exists (B_1 \cup \ldots \cup B_i) Q_jB_j \ldots Q_nB_n$ of $Abs (\phi , i)$.

If $Q_j = \exists$ then $Abs (\varPi , i) = Abs (\varPi , j) = \exists (B_1 \cup \ldots B_i \cup B_j) \ldots Q_nB_n$. Since $Abs (\phi , i) = Abs (\phi , j)$, the claim holds for $Abs (\phi , j)$ by IH.

If $Q_j = \forall$ then, towards a contradiction, assume that, for some T and $T^B$, $T \models _{t} \phi$ and $T^B \subseteq T$ is a pre-model of $Abs (\phi ,j)$, but $T^{B} \not \models _{t} Abs (\phi ,j)$. Then the root of $T^B$ is labelled with $\bot$, and in particular the nodes of all the variables which are existential in $B_j$ with respect to $Abs (\varPi , j)$ are also labelled with $\bot$. These existential variables appear along a single branch $\tau '$ in $T^B$, i.e., $\tau '$ is a partial assignment of the variables in $B_j$. Since $T^B \subseteq T^A$ and $Q_j = \forall$ in $Abs (\varPi , i)$, the root of $T^A$ is labelled with $\bot$ since there is the branch $\tau '$ containing the variables in $B_j$ whose nodes are labelled with $\bot$ in $T^A$. Hence $T^A \not \models _{t} Abs (\phi ,i)$, which is a contradiction to IH. Therefore, we conclude that $T^{B} \models _{t} Abs (\phi ,j)$.    $\square$

If an abstraction $Abs (\phi , i)$ is unsatisfiable then also the original QBF $\phi$ is unsatisfiable due to Proposition 3. We generalize Proposition 1 from CNFs to QBFs and their abstractions. Note that the full abstraction $Abs (\phi , i)$ for $i \,{{:=}}\, n$ of a QBF $\phi$ is a CNF, i.e., it does not contain any universal variables.

Lemma 1

Let $\phi \,{{:=}}\, \varPi . \psi$ and $\phi ' \,{{:=}}\, \varPi . \psi '$ be QBFs with the same prefix $\varPi \,{{:=}}\, Q_1B_1 \ldots Q_iB_i \ldots Q_nB_n$. Then for all i, if $Abs (\phi , i) \equiv _{ t } Abs (\phi ', i)$ then $\phi \equiv _{ t }\phi '$.

Proof

By induction on $i \,{{:=}}\, 0$ up to $i \,{{:=}}\, n$. The base case $i \,{{:=}}\, 0$ is trivial.

As induction hypothesis (IH), assume that the claim holds for some i with $0 \le i < n$, i.e., if $Abs (\phi , i) \equiv _{ t } Abs (\phi ', i)$ then $\phi \equiv _{ t }\phi '$. Let $j = i+1$ and consider $Abs (\phi , j)$ and $Abs (\phi ', j)$, which are abstractions of $Abs (\phi , i)$ and $Abs (\phi ', i)$. We have $Abs (\varPi , i) = \exists (B_1 \cup \ldots \cup B_i) Q_jB_j \ldots Q_nB_n$ and $Abs (\varPi , j) = \exists (B_1 \cup \ldots \cup B_j) \ldots Q_nB_n$. We show that if $Abs (\phi , j) \equiv _{ t } Abs (\phi ', j)$ then $Abs (\phi , i) \equiv _{ t } Abs (\phi ', i)$, and hence also $\phi \equiv _{ t }\phi '$ by IH. Assume that $Abs (\phi , j) \equiv _{ t } Abs (\phi ', j)$. We distinguish cases by the type of $Q_j$ in $Abs (\varPi , i)$. If $Q_j = \exists$ then $Abs (\varPi , i) = Abs (\varPi , j) = \exists (B_1 \cup \ldots B_i \cup B_j) \ldots Q_nB_n$, and hence $Abs (\phi , i) \equiv _{ t } Abs (\phi ', i)$.

If $Q_j = \forall$, then towards a contradiction, assume that $Abs (\phi , j) \equiv _{ t } Abs (\phi ', j)$ but $Abs (\phi , i) \not \equiv _{ t } Abs (\phi ', i)$. Then there exists T such that $T \models _{t} Abs (\phi , i)$ but $T \not \models _{t} Abs (\phi ',i)$. Since $T \not \models _{t} Abs (\phi ',i)$ there exists a pre-model $T^{A} \subseteq T$ of $Abs (\phi ',j)$ such that the root of $T^A$ is labelled with $\bot$, and in particular the nodes of all the variables which are existential in $B_j$ with respect to $Abs (\varPi , j)$ (and universal with respect to $Abs (\varPi , i)$) are also labelled with $\bot$. These existential variables appear along a single branch $\tau '$ in $T^A$, i.e., $\tau '$ is a partial assignment of the variables in $B_j$. Therefore we have $T^A \not \models _{t} Abs (\phi ', j)$. Since $T \models _{t} Abs (\phi ,i)$ and $T^A \subseteq T$, we have $T^A \models _{t} Abs (\phi , j)$ by Proposition 3, which contradicts the assumption that $Abs (\phi , j) \equiv _{ t } Abs (\phi ', j)$.    $\square$

The converse of Lemma 1 does not hold. From the equivalence of two QBFs $\phi$ and $\phi '$ we cannot conclude that the abstractions $Abs (\phi , i)$ and $Abs (\phi ', i)$ are equivalent. In our generalization $\mathsf {QRAT}^{+}$ of the $\mathsf {QRAT}$ system we check whether an outer resolvent of some clause C is implied ($\models _{t}$) by an abstraction of the given QBF. If so then by Lemma 1 the outer resolvent is also implied by the original QBF. Below we prove that this condition is sufficient for the soundness of redundancy removal in $\mathsf {QRAT}^{+}$. To check QBF implication in an incomplete way and in polynomial time, in practice we apply QBF unit propagation, which is an extension of propositional unit propagation, to abstractions of the given QBF.

Definition 8

(universal reduction, UR [15]). Given a QBF $\phi \,{{:=}}\, \varPi . \psi$ and a non-tautological clause C, universal reduction (UR) of C produces the clause $UR (\varPi , C) \,{{:=}}\, C \setminus \{l \in C \mid \mathsf {Q}(\varPi ,l) = \forall , \forall l' \in C, \mathsf {Q}(\varPi ,l') = \exists : \mathsf {var}(l') \le _\varPi \mathsf {var}(l)\}$.

Definition 9

(QBF unit propagation, QUP).QBF unit propagation (QUP) extends UP (Definition 4) by applications of UR. For a QBF $\phi \,{{:=}}\, \varPi . \psi$ and a clause C, let $\varPi . (\psi \wedge \overline{C}) \mathrel {\vdash _{^{_{1\forall }}}}\emptyset$ denote the fact that QUP applied to $\varPi . (\psi \wedge \overline{C})$ produces the empty clause, where $\overline{C}$ is the conjunction of the negation of all the literals in C. If $\varPi . (\psi \wedge \overline{C}) \mathrel {\vdash _{^{_{1\forall }}}}\emptyset$ and additionally $\varPi . \psi \models _{t} \varPi . (\psi \wedge C)$ then we write $\phi \mathrel {\vdash _{^{_{1\forall }}}}C$ to denote that C can be derived from $\phi$ by QUP.

In contrast to UP (Definition 4), deriving the empty clause by QUP by propagating $\overline{C}$ on a QBF $\phi$ is not sufficient to conclude that C is implied by $\phi$.

Example 4

Given the QBF $\varPi . \psi$ with prefix $\varPi \,{{:=}}\, \forall u \exists x$ and CNF $\psi \,{{:=}}\, (u \vee \bar{x}) \wedge (\bar{u} \vee x)$ and the clause $C \,{{:=}}\, (x)$. We have $\varPi . ((u \vee \bar{x}) \wedge (\bar{u} \vee x) \wedge (\bar{x})) \mathrel {\vdash _{^{_{1\forall }}}}\emptyset$ since propagating $\overline{C} = (\bar{x})$ produces $(\bar{u})$, which is reduced to $\emptyset$ by UR. However, $\varPi . \psi \not \models _{t} \varPi . (\psi \wedge C)$ since $\varPi . \psi$ is satisfiable whereas $\varPi . (\psi \wedge C)$ is unsatisfiable. Note that $Abs (\varPi . ((u \vee \bar{x}) \wedge (\bar{u} \vee x) \wedge \bar{x}), 2) \mathrel {\nvdash _{^{_{1\forall }}}}\emptyset$.

To correctly apply QUP for checking whether some clause C (e.g., an outer resolvent) is implied by a QBF $\phi \,{{:=}}\, \varPi . \psi$ and thus avoid the problem illustrated in Example 4, we carry out QUP on a suitable abstraction of $\phi$ with respect to C. Let $i = \max ( levels (\varPi , C))$ be the maximum nesting level of variables that appear in C. We show that if QUP derives the empty clause from the abstraction $Abs (\phi , i)$ augmented by the negated clause $\overline{C}$, i.e., $Abs (\varPi . (\psi \wedge \overline{C}), i) \mathrel {\vdash _{^{_{1\forall }}}}\emptyset$, then we can safely conclude that C is implied by the original QBF, i.e., $\varPi . \psi \models _{t} \varPi . (\psi \wedge C)$. This approach extends failed literal detection for QBF preprocessing [16].

Lemma 2

Let $\varPi . \psi$ be a QBF with prefix $\varPi \,{{:=}}\, Q_1B_1 \ldots Q_nB_n$ and C a clause such that $vars (C) \subseteq B_1$. If $\varPi . (\psi \wedge \overline{C}) \mathrel {\vdash _{^{_{1\forall }}}}\emptyset$ then $\varPi . \psi \equiv _{ t }\varPi . (\psi \wedge C)$.

Proof

By contradiction, assume $T \models _{t} \varPi . \psi$ but $T \not \models _{t} \varPi . (\psi \wedge C)$. Then there is a path $\tau \subseteq T$ such that $\tau (C) = \bot$. Since $vars (C) \subseteq B_1$ and $\varPi . (\psi \wedge \overline{C}) \mathrel {\vdash _{^{_{1\forall }}}}\emptyset$, the QBF $\varPi . (\psi \wedge \overline{C})$ is unsatisfiable and in particular $T \not \models _{t} \varPi . (\psi \wedge \overline{C})$. Since $\tau (C) = \bot$, we have $\tau (\overline{C}) = \top$ and hence $T \models _{t} \varPi . (\psi \wedge \overline{C})$, which is a contradiction.    $\square$

Lemma 3

Let $\varPi . \psi$ be a QBF, C a clause, and $i = \max ( levels (\varPi , C))$. If $Abs (\varPi . (\psi \wedge \overline{C}), i) \mathrel {\vdash _{^{_{1\forall }}}}\emptyset$ then $Abs (\varPi . \psi , i) \equiv _{ t } Abs (\varPi . (\psi \wedge C), i)$.

Proof

The claim follows from Lemma 2 since all variables that appear in C are existentially quantified in $Abs (\varPi . (\psi \wedge \overline{C}), i)$ in the leftmost quantifier block.    $\square$

Lemma 4

Let $\varPi . \psi$ be a QBF, C a clause, and $i = \max ( levels (\varPi , C))$. If $Abs (\varPi . (\psi \wedge \overline{C}), i) \mathrel {\vdash _{^{_{1\forall }}}}\emptyset$ then $\varPi . \psi \equiv _{ t }\varPi . (\psi \wedge C)$.

Proof

By Lemmas 1 and 3.    $\square$

Lemma 4 provides us with the necessary theoretical foundation to lift $\mathsf {AT}$ (Definition 5) from UP, which is applied to CNFs, to QUP, which is applied to suitable abstractions of QBFs. The abstractions are constructed depending on the maximum nesting level of variables in the clause we want to check.

Definition 10

($\mathsf {QAT}$). Let $\phi$ be a QBF, C a clause, and $i = \max ( levels (\varPi , C))$ Clause C has property $\mathsf {QAT}$ (quantified asymmetric tautology) with respect to $\phi$ iff $Abs (\phi , i) \mathrel {\vdash _{^{_{1\forall }}}}C$.

As an immediate consequence from the definition of QUP (Definition 9) and Lemma 3, we can conclude that a clause C has $\mathsf {QAT}$ with respect to a QBF $\varPi . \psi$ if QUP derives the empty clause from the suitable abstraction of $\varPi . \psi$ with respect to C (i.e., $Abs (\varPi . (\psi \wedge \overline{C}), i) \mathrel {\vdash _{^{_{1\forall }}}}\emptyset$). Further, if C has $\mathsf {QAT}$ then we have $\varPi . \psi \equiv _{ t }\varPi . (\psi \wedge C)$ by Lemma 4, i.e., C is implied by the given QBF $\varPi . \psi$.

Example 5

Given the QBF $\phi \,{{:=}}\, \varPi . \psi$ with $\varPi \,{{:=}}\, \forall u_1 \exists x_3 \forall u_2 \exists x_4$ and $\psi \,{{:=}}\, (u_1 \vee \bar{x}_3) \wedge (u_1 \vee \bar{x}_3 \vee x_4) \wedge (\bar{u}_2 \vee \bar{x}_4)$. Clause $(u_1 \vee \bar{x}_3)$ has $\mathsf {QAT}$ with respect to $Abs (\phi , 2)$ with $\max ( levels (C)) = 2$ since $\forall u_2$ is still universal in the abstraction. By QUP clause $(u_1 \vee \bar{x}_3 \vee x_4)$ becomes unit and clause $(\bar{u}_2 \vee \bar{x}_4)$ becomes empty by UR. However, clause $(u_1 \vee \bar{x}_3)$ does not have $\mathsf {AT}$ since $\forall u_2$ is treated as an existential variable in UP, hence clause $(\bar{u}_2 \vee \bar{x}_4)$ does not become empty by UR.

In contrast to $\mathsf {AT}$, $\mathsf {QAT}$ is aware of quantifier structures in QBFs as shown in Example 5. We now generalize $\mathsf {QRAT}$ to $\mathsf {QRAT}^{+}$ by replacing $\mathsf {AT}$ by $\mathsf {QAT}$. Similarly, we generalize $\mathsf {QIOR}$ to $\mathsf {QIOR}^{+}$ by replacing propositional implication ($\models$) and equivalence (Proposition 1), by QBF implication and equivalence (Lemma 4).

Definition 11

($\mathsf {QRAT}^{+}$). Clause C has property $\mathsf {QRAT}^{+}$ on literal $l \in C$ with respect to QBF $\varPi . \psi$ iff, for all $D \in \psi$ with $\bar{l} \in D$, the outer resolvent $\mathsf {OR} (\varPi , C, D,l)$ has $\mathsf {QAT}$ with respect to QBF $\varPi . \psi$.

Definition 12

($\mathsf {QIOR}^{+}$). Clause C has property $\mathsf {QIOR}^{+}$ on literal $l \in C$ with respect to QBF $\varPi . \psi$ iff $\varPi . \psi \equiv _{ t }\varPi . (\psi \wedge \mathsf {OR} (\varPi , C, D, l))$ for all $D \in \psi$ with $\bar{l} \in D$.

If a clause has $\mathsf {QRAT}$ then it also has $\mathsf {QRAT}^{+}$. Moreover, due to Proposition 2, if a clause has $\mathsf {QIOR}$ then it also has $\mathsf {QIOR}^{+}$. Hence $\mathsf {QRAT}^{+}$ and $\mathsf {QIOR}^{+}$ indeed are generalizations of $\mathsf {QRAT}$ and $\mathsf {QIOR}$, which are strict, as we argue below. The soundness of removing redundant clauses and universal literals based on $\mathsf {QIOR}^{+}$ (and on $\mathsf {QRAT}^{+}$) can be proved by the same arguments as original $\mathsf {QRAT}$, which we outline in the following. We refer to an appendix for full proofs [18].

Definition 13

(prefix/suffix assignment [10]). For a QBF $\phi \,{{:=}}\, \varPi . \psi$ and a complete assignment $\tau$ in the assignment tree of $\phi$, the partial prefix and suffix assignments of $\tau$ with respect to variable x, denoted by $\tau ^x$ and $\tau _x$, respectively, are defined as $\tau ^x \,{{:=}}\, \{y \mapsto \tau (y) \mid y \le _\varPi x, y \not = x\}$ and $\tau _x \,{{:=}}\, \{y \mapsto \tau (y) \mid y \not \le _\varPi x\}$.

For a variable x from block $B_i$ of a QBF, Definition 13 allows us to split a complete assignment $\tau$ into three parts $\tau ^xl\tau _x$, where the prefix assignment $\tau ^x$ assigns variables (excluding x) from blocks smaller than or equal to $B_i$, l is a literal of x, and the suffix assignment $\tau _x$ assigns variables from blocks larger than $B_i$.

Prefix and suffix assignments are important for proving the soundness of satisfiability-preserving redundancy removal by $\mathsf {QIOR}^{+}$ (and $\mathsf {QIOR}$). Soundness is proved by showing that certain paths in a model of a QBF can safely be modified based on prefix and suffix assignments, as stated in the following.

Lemma 5

(cf. Lemma 6 in [10]). Given a clause C with $\mathsf {QIOR}^{+}$ with respect to QBF $\phi \,{{:=}}\, \varPi . \psi$ on literal $l \in C$ with $\mathsf {var}(l) = x$. Let T be a model of $\phi$ and $\tau \subseteq T$ be a path in T. If $\tau (C \setminus \{l\}) = \bot$ then $\tau ^x(D) = \top$ for all $D \in \psi$ with $\bar{l} \in D$.

Proof

(sketch, see appendix [18]). Let $D \in \psi$ be a clause with $\bar{l} \in D$ and $R \,{{:=}}\, \mathsf {OR} (\varPi ,C,D,l) = (C \setminus \{l\}) \cup \mathsf {OC} (\varPi , D, \bar{l})$. By Definition 12, we have $\varPi . \psi \equiv _{ t }\varPi . (\psi \wedge \mathsf {OR} (\varPi , C, D, l))$ for all $D \in \psi$ with $\bar{l} \in D$. The rest of the proof considers a path $\tau$ in T and works in the same way as the proof of Lemma 6 in [10].    $\square$

Theorem 3

Given a QBF $\phi \,{{:=}}\, \varPi . \psi$ and a clause $C \in \psi$ with $\mathsf {QIOR}^{+}$ on an existential literal $l \in C$ with respect to QBF $\phi ' \,{{:=}}\, \varPi . \psi '$ where $\psi ' \,{{:=}}\, \psi \setminus \{C\}$. Then $\phi \equiv _{ sat }\phi '$.

Proof

(sketch, see appendix [18]). The proof relies on Lemma 5 and works in the same way as the proof of Theorem 7 in [10]. A model T of $\phi$ is obtained from a model $T'$ of $\phi '$ by flipping the assignment of variable $x = \mathsf {var}(l)$ on a path $\tau$ in $T'$ to satisfy clause C. All $D \in \psi$ with $\bar{l} \in D$ are satisfied by such modified $\tau$.    $\square$

Theorem 4

Given a QBF $\phi _0 \,{{:=}}\, \varPi . \psi$ and $\phi \,{{:=}}\, \varPi . (\psi \cup \{C\})$ where C has $\mathsf {QIOR}^{+}$ on a universal literal $l \in C$ with respect to $\phi _0$. Let $\phi ' \,{{:=}}\, \varPi . (\psi \cup \{C'\})$ with $C' \,{{:=}}\, C \setminus \{l\}$. Then $\phi \equiv _{ sat }\phi '$.

Proof

(sketch, see appendix [18]). The proof relies on Lemma 5 and works in the same way as the proof of Theorem 8 in [10]. A model $T'$ of $\phi '$ is obtained from a model T of $\phi$ by modifying the subtree under the node associated to variable $x = \mathsf {var}(l)$. Suffix assignments of some paths $\tau$ in T are used to construct modified paths in $T'$ under which clause $C'$ is satisfied. All $D \in \psi$ with $\bar{l} \in D$ are still satisfied after such modifications.    $\square$

Analogously to the $\mathsf {QRAT}$ proof system that is based on the $\mathsf {QRAT}$ redundancy property (Definition 6), we obtain the $\mathsf {QRAT}^{+}$ proof system based on property $\mathsf {QRAT}^{+}$ (Definition 11). The system consists of rewrite rules $\mathsf {QRATE}^{+}$, $\mathsf {QRATA}^{+}$, and $\mathsf {QRATU}^{+}$ to eliminate or add redundant clauses, and to eliminate redundant universal literals. On a conceptual level, these rules in $\mathsf {QRAT}^{+}$ are similar to their respective counterparts in the $\mathsf {QRAT}$ system. The extended universal reduction rule $\mathsf {EUR}$ is the same in the $\mathsf {QRAT}$ and $\mathsf {QRAT}^{+}$ systems. In contrast to $\mathsf {QRAT}$, $\mathsf {QRAT}^{+}$ is aware of quantifier structures of QBFs because it relies on the QBF specific property $\mathsf {QAT}$ and QUP instead of on propositional $\mathsf {AT}$ and UP.

The $\mathsf {QRAT}^{+}$ system has the same desirable properties as the original $\mathsf {QRAT}$ system. $\mathsf {QRAT}^{+}$ simulates virtually all inference rules applied in QBF reasoning tools and it is based on redundancy property $\mathsf {QRAT}^{+}$ that can be checked in polynomial time by QUP. Further, $\mathsf {QRAT}^{+}$ allows to represent proofs in the same proof format as $\mathsf {QRAT}$. However, proof checking, i.e., checking whether a clause listed in the proof has $\mathsf {QRAT}^{+}$ on a literal, must be adapted to the use of QBF abstractions and QUP. Consequently, the available $\mathsf {QRAT}$ proof checker QRATtrim [10] cannot be used out of the box to check $\mathsf {QRAT}^{+}$ proofs.

Notably, Skolem functions can be extracted from $\mathsf {QRAT}^{+}$ proofs of satisfiable QBFs in the same way as in $\mathsf {QRAT}$ (consequence of Theorem 3, cf. Corollaries 26 and 27 in [10]). Hence like $\mathsf {QRAT}$, $\mathsf {QRAT}^{+}$ can be integrated in complete QBF workflows that include preprocessing, solving, and Skolem function extraction [5].

5 Exemplifying the Power of $\mathsf {QRAT}^{+}$

In the following, we point out that the $\mathsf {QRAT}^{+}$ system is more powerful than $\mathsf {QRAT}$ in terms of redundancy detection. In particular, we show that the rules $\mathsf {QRATE}^{+}$ and $\mathsf {QRATU}^{+}$ in the $\mathsf {QRAT}^{+}$ system can eliminate certain redundancies that their counterparts $\mathsf {QRATE}$ and $\mathsf {QRATU}$ cannot eliminate.

Definition 14

For $n \ge 1$, let $\varPhi _{C}(n) \,{{:=}}\, \varPi _{C}(n). \psi _{C}(n)$ be a class of QBFs with prefix $\varPi _{C}(n)$ and CNF $\psi _{C}(n)$ defined as follows.

Example 6

For $n {:=} 1$, we have $\varPhi _{C}(n)$ with prefix $\varPi _{C}(n) {:=} \exists x_{1}, x_{2} \forall u_{1} \exists x_{3} \forall u_{2} \exists x_{4}$ and CNF $\psi _{C}(n) {:=} \mathcal {C}(0)$ with $\mathcal {C}(0) {:=} \bigwedge _{j {:=} 0}^{6} C_{0,j}$ as follows.

Proposition 4

For $n \ge 1$, $\mathsf {QRATE}^{+}$ can eliminate all clauses in $\varPhi _{C}(n)$ whereas $\mathsf {QRATE}$ cannot eliminate any clause in $\varPhi _{C}(n)$.

Proof

(sketch). For i and k with $i \not = k$, the sets of variables in $\mathcal {C}(i)$ and $\mathcal {C}(k)$ are disjoint. Thus it suffices to prove the claim for an arbitrary $\mathcal {C}(i)$. Clause $C_{i,0}$ has $\mathsf {QRAT}^{+}$ on literal $x_{4i + 1}$ and can be removed. The relevant outer resolvents are $\mathsf {OR} _{0,2} = \mathsf {OR} (\varPi _{C}(n), C_{i,0}, C_{i,2}, x_{4i + 1})$ and $\mathsf {OR} _{0,6} = \mathsf {OR} (\varPi _{C}(n), C_{i,0}, C_{i,6}, x_{4i + 1})$, and we have $\mathsf {OR} _{0,2} = \mathsf {OR} _{0,6} = (u_{2i + 1} \vee \lnot x_{4i + 3})$. Since $\max ( levels (\mathsf {OR} _{0,2})) = \max ( levels (\mathsf {OR} _{0,6})) = 3$, we apply QUP to the abstraction $Abs (\varPhi _{C}(n), 3)$. Note that variable $u_{2i + 2}$ from block $B_4$ still is universal in the prefix of $Abs (\varPhi _{C}(n), 3)$. Propagating $\overline{\mathsf {OR} _{0,2}}$ and $\overline{\mathsf {OR} _{0,6}}$, respectively, in either case makes $C_{i,4}$ unit, finally $C_{i,5}$ becomes empty under the derived assignment $x_{4i + 4}$ since UR reduces the literal $\lnot u_{2i + 2}$. After removing $C_{i,0}$, clauses $C_{i,2}$ and $C_{i,6}$ trivially have $\mathsf {QRAT}^{+}$ on $\lnot x_{4i + 1}$. Then $C_{i,1}$ has $\mathsf {QRAT}^{+}$ on $x_{4i + 3}$. Finally, the remaining clauses trivially have $\mathsf {QRAT}^{+}$. In contrast to that, $\mathsf {QRATE}$ cannot eliminate any clause in $\varPhi _{C}(n)$. Clause $C_{i,5}$ does not become empty by UP since all variables are existential. The claim can be proved by case analysis of all possible outer resolvents.    $\square$

Definition 15

For $n \ge 1$, let $\varPhi _{L}(n) {:=} \varPi _{L}(n). \psi _{L}(n)$ be a class of QBFs with prefix $\varPi _{L}(n)$ and CNF $\psi _{L}(n)$ defined as follows.

Proposition 5

For $n \ge 1$, $\mathsf {QRATU}^{+}$ can eliminate the entire quantifier block $\forall B_1$ in $\varPhi _{L}(n)$ whereas $\mathsf {QRATU}$ cannot eliminate any universal literals in $\varPhi _{L}(n)$.

Proof

(sketch, see appendix [18]). Formulas $\varPhi _{L}(n)$ are constructed based on a similar principle as $\varPhi _{C}(n)$ in Definition 14. E.g., clauses $C_{i,0}$ and $C_{i,1}$ have $\mathsf {QRAT}^{+}$ but not $\mathsf {QRAT}$ on literals $\lnot u_{3i+2}$ and $\lnot u_{3i+1}$. During QUP, clauses $C_{i,5}$ and $C_{i,7}$ become empty only due to UR, which is not possible when using UP.    $\square$

6 Proof Theoretical Impact of $\mathsf {QRAT}$ and $\mathsf {QRAT}^{+}$

As argued in the context of interference-based proof systems [6], certain proof steps may become applicable in a proof system only after redundant parts of the formula have been eliminated. We show that redundancy elimination by $\mathsf {QRAT}^{+}$ or $\mathsf {QRAT}$ can lead to exponentially shorter proofs in the resolution based LQU$^+$-resolution [1] QBF calculus. Note that we do not compare the power of $\mathsf {QRAT}$ or $\mathsf {QRAT}^{+}$ as proof systems themselves, but the impact of redundancy elimination on other proof systems. The following result relies only on $\mathsf {QRATU}$, i.e., it does not require the more powerful redundancy property $\mathsf {QRATU}^{+}$ in $\mathsf {QRAT}^{+}$.

LQU$^+$-resolution is a calculus that generalizes traditional Q-resolution [15]. It allows to generate resolvents on both existential and universal variables and admits tautological resolvents of a certain kind. LQU$^+$-resolution is among the strongest resolution calculi currently known [1, 2], yet the following class of QBFs provides an exponential lower bound on the size of LQU$^+$-resolution proofs.

Definition 16

([2]). For $n > 1$, let $\varPhi _{Q}(n) {:=} \varPi _{Q}(n). \psi _{Q}(n)$ be the QUParity QBFs with $\varPi _{Q}(n) {:=} \exists x_1, \ldots , x_n \forall z_1, z_2 \exists t_2, \ldots , t_n$ and $\psi _{Q}(n) {:=} C_0 \wedge C_1 \wedge \bigwedge _{i {:=} 2}^{n} \mathcal {C}(i)$ where $C_0 {:=} (z_1 \vee z_2 \vee t_n)$, $C_1 {:=} (\bar{z}_1 \vee \bar{z}_2 \vee \bar{t}_n)$, and $\mathcal {C}(i) {:=} \bigwedge _{j {:=} 0}^{7} C_{i,j}$:

Any refutation of $\varPhi _{Q}(n)$ in LQU$^+$-resolution is exponential in n [2]. The QUParity formulas are a modification of the related LQParity formulas [2]. An LQParity formula is obtained from a QUParity formula $\varPhi _{Q}(n)$ by replacing $\forall z_1,z_2$ in prefix $\varPi _{Q}(n)$ by $\forall z$ and by replacing every occurrence of the literal pairs $z_1 \vee z_2$ and $\bar{z}_1 \vee \bar{z}_2$ in the clauses in $\psi _{Q}(n)$ by the literal z and $\bar{z}$, respectively.

Proposition 6

$\mathsf {QRATU}$ can eliminate either variable $z_1$ or $z_2$ from a QUParity formula $\varPhi _{Q}(n)$ to obtain a related LQParity formula in polynomial time.

Proof

We eliminate $z_2$ ($z_1$ can be eliminated alternatively) in a polynomial number of $\mathsf {QRATU}$ steps. Every clause C with $z_2 \in C$ has $\mathsf {QRAT}$ on $z_2$ since $\{z_1, \bar{z}_1\} \subseteq \mathsf {OR}$ for all outer resolvents $\mathsf {OR}$. UP immediately detects a conflict when propagating $\overline{\mathsf {OR}}$. After eliminating all literals $z_2$, the clauses containing $\bar{z}_2$ trivially have $\mathsf {QRAT}$ on $\bar{z}_2$, which can be eliminated. Finally, $z_1$ including all of its occurrences is renamed to z.    $\square$

In the proof above the universal literals can be eliminated by $\mathsf {QRATU}$ in any order. Hence in this case the non-confluence [9, 14] of rewrite rules in the $\mathsf {QRAT}$ and $\mathsf {QRAT}^{+}$ systems is not an issue. LQU$^+$-resolution has polynomial proofs for LQParity formulas [2]. Hence the combination of $\mathsf {QRATU}$ and LQU$^+$-resolution results in a calculus that is more powerful than LQU$^+$-resolution. A related result [13] was obtained for the combination of $\mathsf {QRATU}$ and the weaker QU-resolution calculus [22].

7 Experiments

We implemented $\mathsf {QRAT}^{+}$ redundancy removal in a tool called for QBF preprocessing.² It applies rules $\mathsf {QRATE}^{+}$ and $\mathsf {QRATU}^{+}$ to remove redundant clauses and universal literals. We did not implement clause addition ($\mathsf {QRATA}^{+}$) or extended universal reduction ($\mathsf {EUR}$). is the first implementation of $\mathsf {QRAT}^{+}$ and $\mathsf {QRAT}$ for QBF preprocessing. The preprocessors HQSpre [24] and Bloqqer [10] (which generates partial $\mathsf {QRAT}$ proofs to trace preprocessing steps) do not apply $\mathsf {QRAT}$ to eliminate redundancies. The following experiments were run on a cluster of Intel Xeon CPUs (E5-2650v4, 2.20 GHz) running Ubuntu 16.04.1. We used the benchmarks from the PCNF track of the QBFEVAL’17 competition. In terms of scheduling the non-confluent (cf. [9, 14]) rewrite rules $\mathsf {QRATE}^{+}$ and $\mathsf {QRATU}^{+}$, we have not yet optimized . Moreover, in general large numbers of clauses in formulas may cause run time overhead. In this respect, our implementation leaves room for improvements.

Table 1. Solved instances (S), solved unsatisfiable ($\bot$) and satisfiable ones ($\top$), and total wall clock time in kiloseconds (K) including time outs on instances from QBFEVAL’17. Different combinations of preprocessing by Bloqqer, HQSpre, and our tool .

We illustrate the impact of QBF preprocessing by $\mathsf {QRAT}^{+}$ and $\mathsf {QRAT}$ on the performance of QBF solving. To this end, we applied in addition to the state of the art QBF preprocessors Bloqqer and HQSpre. In the experiments, first we preprocessed the benchmarks using Bloqqer and HQSpre, respectively, with a generous limit of two hours wall clock time. We considered 39 and 42 formulas where Bloqqer and HQSpre timed out, respectively, in their original form. Then we applied to the preprocessed formulas with a soft wall clock time limit of 600 seconds. When reaches the limit, it prints the formula with redundancies removed that have been detected so far. These preprocessed formulas are then solved. Table 1 shows the performance of our solver DepQBF [17] in addition to the top-performing solvers³ RAReQS [11], CAQE [20], and Qute [19] from QBFEVAL’17, using limits of 7 GB and 1800 s wall clock time. The solvers implement different solving paradigms such as expansion or resolution-based QCDCL. The results clearly indicate the benefits of preprocessing by . The number of solved instances increases. Qute is an exception to this trend. We conjecture that blurs the formula structure in addition to Bloqqer and HQSpre, which may be harmful to Qute.

We emphasize that we hardly observed a difference in the effectiveness of redundancy removal by $\mathsf {QRAT}^{+}$ and $\mathsf {QRAT}$ on the considered benchmarks. The benefits of shown in Table 1 are due to redundancy removal by $\mathsf {QRAT}$ already, and not by $\mathsf {QRAT}^{+}$. However, on additional 672 instances from class Gent-Rowley (encodings of the Connect Four game) available from QBFLIB, $\mathsf {QRATE}^{+}$ on average removed 54% more clauses than $\mathsf {QRATE}$. We attribute this effect to larger numbers of quantifier blocks in the Gent-Rowley instances (median 73, average 79) compared to QBFEVAL’17 (median 3, average 27). The advantage of QBF abstractions in the $\mathsf {QRAT}^{+}$ system is more pronounced on instances with many quantifier blocks.

8 Conclusion

We presented $\mathsf {QRAT}^{+}$, a generalization of the $\mathsf {QRAT}$ proof system, that is based on a more powerful QBF redundancy property. The key difference between the two systems is the use of QBF specific unit propagation in contrast to propositional unit propagation. Due to this, redundancy checking in $\mathsf {QRAT}^{+}$ is aware of quantifier structures in QBFs, as opposed to $\mathsf {QRAT}$. Propagation in $\mathsf {QRAT}^{+}$ potentially benefits from the presence of universal variables in the underlying formula. This is exploited by the use of abstractions of QBFs, for which we developed a theoretical framework, and from which the soundness of $\mathsf {QRAT}^{+}$ follows. By concrete classes of QBFs we demonstrated that $\mathsf {QRAT}^{+}$ is more powerful than $\mathsf {QRAT}$ in terms of redundancy detection. Additionally, we reported on proof theoretical improvements of a certain resolution based QBF calculus made by $\mathsf {QRAT}$ (or $\mathsf {QRAT}^{+}$) redundancy removal. A first experimental evaluation illustrated the potential of redundancy elimination by $\mathsf {QRAT}^{+}$.

As future work, we plan to implement a workflow for checking $\mathsf {QRAT}^{+}$ proofs and extracting Skolem functions similar to $\mathsf {QRAT}$ proofs [10]. In our $\mathsf {QRAT}^{+}$ preprocessor we currently do not apply a specific strategy to handle the non-confluence of rewrite rules. We want to further analyze the effects of non-confluence as it may have an impact on the amount of redundancy detected. In our tool we considered only redundancy removal. However, to get closer to the full power of the $\mathsf {QRAT}^{+}$ system, it may be beneficial to also add redundant clauses or universal literals to a formula.