Local Redundancy in SAT: Generalizations of Blocked Clauses

TL;DR

This paper introduces a semantic and syntactic framework for local redundancy properties in SAT, generalizing blocked clauses, with theoretical characterizations and complexity analysis.

Contribution

It presents the most general local redundancy property via semantic blocking and introduces set-blocking and super-blocking notions, expanding the understanding of clause elimination.

Findings

Semantic blocking is the most general local redundancy property.

Super-blocking coincides with semantic blocking.

Complexity analysis of new redundancy properties.

Abstract

Clause-elimination procedures that simplify formulas in conjunctive normal form play an important role in modern SAT solving. Before or during the actual solving process, such procedures identify and remove clauses that are irrelevant to the solving result. These simplifications usually rely on so-called redundancy properties that characterize cases in which the removal of a clause does not affect the satisfiability status of a formula. One particularly successful redundancy property is that of blocked clauses, because it generalizes several other redundancy properties. To find out whether a clause is blocked---and therefore redundant---one only needs to consider its resolution environment, i.e., the clauses with which it can be resolved. For this reason, we say that the redundancy property of blocked clauses is local. In this paper, we show that there exist local redundancy properties that are even more general than blocked clauses. We present a semantic notion of blocking and prove that it constitutes the most general local redundancy property. We furthermore introduce the syntax-based notions of set-blocking and super-blocking, and show that the latter coincides with our semantic blocking notion. In addition, we show how semantic blocking can be alternatively characterized via Davis and Putnam's rule for eliminating atomic formulas. Finally, we perform a detailed complexity analysis and relate our novel redundancy properties to prominent redundancy properties from the literature.

Equations

$$\{(F,C)\mid \text{F is a formula and C is a tautology}\}$$

Full text

This work has been supported by the Austrian Science Fund (FWF) under projects W1255-N23 and S11408-N23.

Introduction

Over the last two decades, there has been enormous progress in the performance of SAT solvers, i.e., decision procedures for the satisfiability problem of propositional logic (SAT) [DBLP:series/faia/2009-185]. As a consequence, SAT solvers have become attractive reasoning engines in many user domains like the verification of hardware and software [vizel15] as well as in the backends of other reasoning tools like SMT solvers [DBLP:series/faia/BarrettSST09], QBF solvers [janota16_qbfcegar, samulowitz05_usingsatinqbf], or even first-order theorem provers [DBLP:conf/cade/RegerSV15]. In such applications, however, SAT solvers often reach their limits, motivating the quest for more efficient SAT techniques.

One successful approach to improving the performance of SAT solvers is the use of clause-elimination procedures. Either before (“preprocessing”) or during the actual solving (“inprocessing”) such procedures simplify a given formula in conjunctive normal form (CNF) by removing clauses that are irrelevant to the outcome of the solving process [OptimizedBlockedClauseDecomposition, DBLP:journals/corr/Chen15o, BlockedClauseDecomposition, ClauseEliminationJournal, DBLP:conf/sat/IserMS15, BlockedClauseEliminationJournal, Inprocessing, DBLP:conf/sat/MantheyPW13]. To distinguish the irrelevant from the relevant, they usually rely on so-called redundancy properties that characterize cases in which certain clauses can be removed from a formula without affecting its satisfiability status [ClauseEliminationJournal, Inprocessing]. For instance, a clause-elimination procedure that is based on the simple redundancy property of tautologies identifies and removes tautological clauses—clauses that contain two complementary literals. As these clauses are true regardless of a particular truth assignment, their removal does not influence the outcome of the solving process.

A particularly useful redundancy property is that of blocked clauses [BlockedClauseElimination, BlockedClauses]. Informally, a clause $C$ is blocked in a CNF formula $F$ if it contains a literal $l$ such that all possible resolvents of $C$ upon $l$ (with clauses from $F$) are tautologies. The elimination of blocked clauses considerably improves the performance of modern SAT solvers [BlockedClauseElimination, DBLP:conf/sat/MantheyPW13]. Moreover, blocked clauses provide the basis for blocked-clause decomposition, a technique that splits a CNF formula into two parts that become solvable by blocked-clause elimination [BlockedClauseDecomposition]. Blocked-clause decomposition is successfully used for gate extraction, for efficiently finding backbone variables, and for the detection of implied binary equivalences [OptimizedBlockedClauseDecomposition, DBLP:conf/sat/IserMS15]. The winner of the SAT-Race 2015 competition, the solver $\mathsf{abcdSAT}$ [DBLP:journals/corr/Chen15o], uses blocked-clause decomposition as core technology.

Part of the reason for the success of blocked clauses is the fact that they generalize several other well-known redundancy properties such as those of pure literals [davis60_a_computing_procedure] or the above-mentioned tautologies. This means that a tool for blocked-clause elimination implicitly performs the elimination of pure literals and tautologies (and even more aggressive formula simplifications on top). A closer look at the definition of blocked clauses reveals that to check whether a clause is blocked, it suffices to consider only its resolution environment, i.e., the clauses with which it can be resolved. Because of this, we say that the blocked-clauses redundancy property is local. Their locality aspect makes blocked clauses particularly effective when dealing with large formulas in which the resolution environments of clauses are small.

These success stories motivate us to have a closer look at local redundancy properties in general and at blocked clauses in particular. We show in this paper that blocked clauses do not constitute the most general concept of a local redundancy property. In particular, we first present some observations on blocked clauses and provide examples of redundant clauses that are not blocked, yet their redundancy can be identified by considering only their resolution environment. We next use these observations to derive a semantic notion of blocking for which we show that it constitutes the most general local redundancy property. To bring this semantic notion of blocking closer to practical SAT solving, we then introduce the syntax-based redundancy properties of set-blocked clauses and super-blocked clauses—both are strictly more general than traditional blocked clauses and for super-blocking we prove that it coincides with our semantic blocking notion.

After introducing the new redundancy properties, we present an alternative syntactic characterization of semantic blocking based on Davis and Putnam’s rule for eliminating atomic formulas [davis60_a_computing_procedure]—a resolution-based rewriting rule that is also known as variable elimination [effective_preprocessing_een05] in the context of SAT solving. This characterization further clarifies the connection between traditional blocking and semantic blocking. We then proceed by analyzing the complexity of deciding whether a clause is redundant with respect to our novel redundancy properties. Our complexity analysis gives rise to a whole family of redundancy properties that are obtained by restricting the notions of set-blocking and super-blocking in certain ways. Finally, we outline the relationship of the new redundancy properties to prominent redundancy properties from the literature before concluding with an outlook to future work.

A preliminary version of this paper appeared in the proceedings of IJCAR 2016 [superblocked_clauses]. Besides several extensions of the text, this version now includes the full proofs of our complexity results while the conference paper [superblocked_clauses] contained only proof sketches. In addition, we introduce an alternative characterization of semantic blocking based on variable elimination (cf. Section LABEL:sec:ve).

1. Preliminaries

We consider propositional formulas in conjunctive normal form (CNF) which are defined as follows. A literal is either a Boolean variable $x$ (a positive literal) or the negation $\neg x$ of a variable $x$ (a negative literal). For a literal $l$, we define $\bar{l}=\neg x$ if $l=x$ and $\bar{l}=x$ if $l=\neg x$. Accordingly, for a set $L$ of literals, we define $\bar{L}=\{\bar{l}\mid l\in L\}$. A clause is a disjunction of literals. A formula is a conjunction of clauses. We identify a clause with a set of literals and a formula with a set of clauses. A tautology is a clause that contains both $l$ and $\bar{l}$ for some literal $l$. For a literal, clause, or formula $E$, $\mathit{var}(E)$ denotes the set of variables occurring in $E$. For convenience, we often treat $\mathit{var}(E)$ as a variable if $E$ is a literal. For a set $L$ of literals and a formula $F$, we denote by $F_{L}$ the set of all clauses in $F$ that contain a literal of $L$, i.e., F_{L}=\{C\mid\text{C\in F$and$C\cap L\neq\emptyset}\}. In case $L$ is a singleton set of the form $\{l\}$, we sometimes write $F_{l}$ instead of $F_{\{l\}}$.

An assignment is a function from a set of variables to the truth values 1 (true) and 0 (false). An assignment is total with respect to a formula if it assigns a truth value to all variables occurring in the formula. Unless stated otherwise, we do not assume assignments to be total. Assignments are extended from variables to literals by defining $\tau(l)=\tau(\mathit{var}(l))$ if the literal $l$ is positive and by defining $\tau(l)=1-\tau(\mathit{var}(l))$ if $l$ is negative. Given an assignment $\tau$ that assigns a truth value to a literal $l$, we denote by $\tau_{l}$ the assignment obtained from $\tau$ by interchanging (“flipping”) the truth value of $l$, i.e., by defining $\tau_{l}(x)=1-\tau(x)$ if $x=\mathit{var}(l)$ and $\tau_{l}(x)=\tau(x)$ otherwise.

A literal $l$ is satisfied by an assignment $\tau$ if $\tau(l)=1$. A clause is satisfied by an assignment $\tau$ if it contains a literal that is satisfied by $\tau$. Finally, a formula is satisfied by an assignment $\tau$ if all of its clauses are satisfied by $\tau$. A formula is satisfiable if there exists an assignment that satisfies it. Two formulas are logically equivalent if they are satisfied by the same total assignments. Two formulas $F$ and $F^{\prime}$ are satisfiability equivalent if either both $F$ and $F^{\prime}$ are satisfiable or both $F$ and $F^{\prime}$ are unsatisfiable. We sometimes say that an assignment $\tau$ falsifies a literal $l$ if $\tau(l)=0$. Accordingly $\tau$ falsifies a clause $C$ if $\tau$ falsifies all literals of $C$.

Given two clauses $C$ and $D$ together with a literal $l\in C$ such that $\bar{l}\in D$, the clause $(C\setminus\{l\})\cup(D\setminus\{\bar{l}\})$ is the resolvent of $C$ and $D$ upon $l$ and denoted by $C\otimes_{l}D$. Given a formula $F$ and a clause $C$, the resolution environment of $C$ in $F$ is the set of all clauses in $F$ that can be resolved with $C$:

{defi}

The resolution environment of a clause $C$ with respect to a formula $F$ is the clause set $\mathit{env}_{F}(C)=\{D\in F\mid\exists\,l\in D\text{ such that }\bar{l}\in C\}$.

Given a formula $F$ and a clause $C$, we call the variables in $\mathit{var}(C)$ the local variables and the variables in $\mathit{var}(\mathit{env}_{F}(C))\setminus\mathit{var}(C)$ the external variables. We denote the set of external variables by $\mathit{ext}_{F}(C)$.

Next, we formally introduce redundancy of clauses. Intuitively, a clause $C$ is redundant with respect to a formula $F$ if neither its addition to $F$ nor its removal from $F$ changes the satisfiability or unsatisfiability of $F$.

{defi}

A clause $C$ is redundant with respect to a formula $F$ if $F\setminus\{C\}$ and $F\cup\{C\}$ are satisfiability equivalent. A redundancy property is a set of pairs $(F,C)$ where $C$ is redundant with respect to $F$. Finally, for two redundancy properties $\mathcal{P}_{1}$ and $\mathcal{P}_{2}$, $\mathcal{P}_{1}$ is more general than $\mathcal{P}_{2}$ if $\mathcal{P}_{2}\subseteq\mathcal{P}_{1}$, i.e., if every pair $(F,C)\in\mathcal{P}_{2}$ is also contained in $\mathcal{P}_{1}$. If $\mathcal{P}_{2}\subset\mathcal{P}_{1}$, then $\mathcal{P}_{1}$ is strictly more general than $\mathcal{P}_{2}$.

{exa}

Consider the formula $F=\{(a\lor b),(\neg a\lor\neg b)\}$. The clause $C=(\neg a\lor\neg b)$ is redundant with respect to $F$ since $F\setminus\{C\}$ and $F\cup\{C\}$ are satisfiability equivalent (although they are not logically equivalent). Moreover, the set

[TABLE]

is a redundancy property since for every formula $F$ and every tautology $C$, $F\setminus\{C\}$ and $F\cup\{C\}$ are satisfiability equivalent.

Note that a clause $C$ is not redundant with respect to a formula $F$ if and only if $F\setminus\{C\}$ is satisfiable and $F\cup\{C\}$ is unsatisfiable. To prove that $C$ is redundant with respect to $F$, it therefore suffices to show that satisfiability of $F\setminus\{C\}$ implies satisfiability of $F\cup\{C\}$. Redundancy properties as defined above yield the basis not only for clause-elimination but also for clause-addition procedures [Inprocessing].

2. Observations on Blocked Clauses

Following Heule et al. [ClauseEliminationJournal] we recapitulate the definition of blocked clauses. In the rest of the paper, we refer to this kind of blocked clauses as literal-blocked clauses. Motivated by the examples given in this section, we then generalize this traditional notion of blocking to more powerful redundancy properties.

{defi}

A clause $C$ is blocked by a literal $l\in C$ in a formula $F$ if $C\cup(D\setminus\{\bar{l}\})$ is a tautology for each clause $D\in F_{\bar{l}}$. A clause $C$ is literal-blocked in $F$ if there exists a literal that blocks $C$ in $F$. By $\mathsf{BC}$ we denote the set \{(F,C)\mid\text{C$is literal-blocked in$F}\}.

{exa}

Consider the formula $F=\{(\neg a\lor c),(\neg b\lor\neg a)\}$ and the clause $C=(a\lor b)$. The literal $b$ blocks $C$ in $F$ since the only clause in $F$ that contains $\neg b$ is the clause $D$ with $D=(\neg b\lor\neg a)$ and further $C\cup(D\setminus\{\bar{l}\})=(a\lor b\lor\neg a)$ is a tautology.

Note that this definition of literal-blocked clauses differs slightly from Kullman’s original definition [BlockedClauses]. The original definition requires that all resolvents of $C$ upon a literal $l$ are tautologies. However, it is not necessary to remove $l$ from $C\cup(D\setminus\{\bar{l}\})$—as would be the case in the resolvent of $C$ and $D$—to guarantee redundancy of literal-blocked clauses. If $l$ is not removed from $C$, every tautology $C$ is also a literal-blocked cause, which is not the case for the original definition.

Proposition 1**.**

$\mathsf{BC}$* is a redundancy property.*

Proposition 1 paraphrases results from Heule et al. [ClauseEliminationJournal] and actually follows from our present results given later on (namely from Proposition LABEL:thm:bc_subset_setb and Corollary LABEL:thm:setb_is_a_local_redundancy_property). To see that blocked clauses are redundant, let $C$ be a clause that is blocked by a literal $l$ in a formula $F$ and assume that some assignment $\tau$ satisfies $F\setminus\{C\}$ but falsifies $C$. We can then easily turn $\tau$ into a satisfying assignment $\tau_{l}$ of $C$ by flipping the truth value of $l$.

This flipping could only possibly falsify some of the clauses in $F\setminus\{C\}$ that contain $\bar{l}$, but the condition that $l$ blocks $C$ guarantees that these clauses stay satisfied: Let $D$ be such a clause that contains $\bar{l}$. Then, since $C\cup(D\setminus\{\bar{l}\})$ is a tautology, either $D$ is itself a tautology (and therefore trivially satisfied) or it contains a literal $l^{\prime}\neq l$ such that $\bar{l}^{\prime}\in C$. In the latter case, since $\tau$ falsifies $C$, it must satisfy $l^{\prime}$ and since $\tau_{l}$ agrees with $\tau$ on all literals but $l$, $\tau_{l}$ is a satisfying assignment of $F\cup\{C\}$. Hence, $C$ is redundant with respect to $F$.

Next, we illustrate with an example how a satisfying assignment of $F\cup\{C\}$ can be obtained from one of $F\setminus\{C\}$ [ClauseEliminationJournal]. This approach is used to obtain a satisfying assignment of the original formula when literal-blocked clauses have been removed during pre- or inprocessing: Suppose a SAT solver gets an input formula $F$ and removes literal-blocked clauses to obtain a simplified formula $F^{\prime}$. The solver then proceeds by searching for a satisfying assignment of $F^{\prime}$. Once it has found such an assignment, it can easily turn it into a satisfying assignment of the original formula $F$.

{exa}

Consider again the formula $F=\{(\neg a\lor c),(\neg b\lor\neg a)\}$ and the clause $C=(a\lor b)$ from Example 2. We already know that $b$ blocks $C$ in $F$. So, let $\tau$ denote the assignment that falsifies the variables $a$, $b$, and $c$. Clearly, $\tau$ satisfies $F$ but falsifies $C$. Now, the assignment $\tau_{b}$, obtained from $\tau$ by flipping the truth value of $b$, satisfies not only $C$ but also all clauses of $F$: The only clause that could have been falsified by flipping the truth value of $b$ is $(\neg b\lor\neg a)$. But, since $\tau$ satisfies $\neg a$ and $\tau_{b}$ agrees with $\tau$ on all variables except $b$, $\tau_{b}$ satisfies $F\cup\{C\}$.

Literal-blocked clauses generalize many other redundancy properties like pure literal or tautology [ClauseEliminationJournal]. One of their particularly important properties is that for testing whether some clause $C$ is literal-blocked in a formula $F$ it suffices to consider only those clauses of $F$ that can be resolved with $C$, i.e., the clauses in the resolution environment $\mathit{env}_{F}(C)$ of $C$.

This raises the question whether there exist redundant clauses that are not blocked but whose redundancy can be identified by considering only their resolution environment. As shown in the next example, this is indeed the case:

{exa}

Let $C=(a\lor b)$ and $F$ an arbitrary formula with the resolution environment $\mathit{env}_{F}(C)=\{(x\lor b\lor\neg a),(\neg b\lor\neg x),(\neg b\lor a)\}$ (cf. Fig. 1). The clause $C$ is not literal-blocked in $F$ but redundant: Suppose there exists an assignment $\tau$ that satisfies $F$ but falsifies $C$. Then, $\tau$ must satisfy either $x$ or $\neg x$. If $\tau(x)=1$, then $C$ can be satisfied by flipping the truth value of $a$, resulting in assignment $\tau^{\prime}=\tau_{a}$. Since $\tau^{\prime}(x)=1$, the clause $(x\lor b\lor\neg a)$ stays satisfied. In contrast, if $\tau(x)=0$, we can satisfy $C$ by the assignment $\tau^{\prime\prime}$ obtained from $\tau$ by flipping the truth values of both $a$ and $b$: The fact that $\tau^{\prime\prime}(b)=1$ guarantees that $(x\lor b\lor\neg a)$ stays satisfied whereas $\tau^{\prime\prime}(x)=0$ and $\tau^{\prime\prime}(a)=1$ guarantee that both $(\neg b\lor\neg x)$ and $(\neg b\lor a)$ stay satisfied. Since flipping the truth values of literals in $C$ does not affect the truth of clauses outside the resolution environment $\mathit{env}_{F}(C)$ of $C$, we obtain in both cases a satisfying assignment of $F$.

3. A Semantic Notion of Blocking

In the examples of the preceding section, when arguing that a clause $C$ is redundant with respect to some formula $F$, we showed that every assignment $\tau$ that satisfies $F\setminus\{C\}$ but falsifies $C$ can be turned into a satisfying assignment $\tau^{\prime}$ of $F\cup\{C\}$ by flipping the truth values of certain literals in $C$. Since this flipping only affects the truth of clauses in $\mathit{env}_{F}(C)$, it suffices to make sure that $\tau^{\prime}$ satisfies $\mathit{env}_{F}(C)$ in order to guarantee that it satisfies $F\cup\{C\}$. This naturally leads to the following semantic notion of blocking:

{defi}

A clause $C$ is semantically blocked in a formula $F$ if, for every satisfying assignment $\tau$ of $\mathit{env}_{F}(C)$, there exists a satisfying assignment $\tau^{\prime}$ of $\mathit{env}_{F}(C)\cup\{C\}$ such that $\tau(v)=\tau^{\prime}(v)$ for all $v\notin\mathit{var}(C)$. We denote the set \{(F,C)\mid\text{C$is semantically blocked in$F}\} by $\mathsf{SEM_{BC}}$.

Note that clause $C$ in Example 2 is semantically blocked in $F$. Note also that a clause is semantically blocked if its resolution environment is unsatisfiable.

Theorem 2**.**

$\mathsf{SEM_{BC}}$* is a redundancy property.*

Proof 3.1**.**

Let $F$ be a formula and $C$ a clause that is semantically blocked in $F$. We show that $F\cup\{C\}$ is satisfiable if $F\setminus\{C\}$ is satisfiable. Suppose there exists a satisfying assignment $\tau$ of $F\setminus\{C\}$. We proceed by a case distinction.

Case 1:* $C$ contains a literal $l$ with $\mathit{var}(l)\notin\mathit{var}(F\setminus\{C\})$. Then, $\tau$ can be easily extended to a satisfying assignment $\tau^{\prime}$ of $F\cup\{C\}$ by defining that $\tau^{\prime}$ satisfies $l$.*

Case 2:* $\mathit{var}(C)\subseteq\mathit{var}(F\setminus\{C\})$. In this case, $\tau$ is a total assignment with respect to $F\cup\{C\}$. Suppose that $\tau$ falsifies $C$. It follows that $C$ is not a tautology and so it does not contain a literal $l$ such that $\bar{l}\in C$, hence $C\notin\mathit{env}_{F}(C)$. Thus, $\mathit{env}_{F}(C)\subseteq F\setminus\{C\}$ and so $\tau$ satisfies $\mathit{env}_{F}(C)$. Since $C$ is semantically blocked in $F$, there exists a satisfying assignment $\tau^{\prime}$ of $\mathit{env}_{F}(C)\cup\{C\}$ such that $\tau(v)=\tau^{\prime}(v)$ for all $v\notin\mathit{var}(C)$. Now, since $\tau^{\prime}(v)$ differs from $\tau$ only on variables in $\mathit{var}(C)$, the only clauses in $F$ that could possibly be falsified by $\tau^{\prime}$ are those with a literal $\bar{l}$ such that $l\in C$. But those are exactly the clauses in $\mathit{env}_{F}(C)$, so $\tau^{\prime}$ satisfies $F\cup\{C\}$.*

Hence, $C$ is redundant with respect to $F$ and thus $\mathsf{SEM_{BC}}$ is a redundancy property. ∎

If a clause $C$ is redundant with respect to some formula $F$ and if this redundancy can be identified by considering only its resolution environment in $F$, then we expect $C$ to be redundant with respect to every formula $F^{\prime}$ in which $C$ has the same resolution environment as in $F$. This leads us to the notion of local redundancy properties:

{defi}

A redundancy property $\mathcal{P}$ is local if, for every clause $C$ and any two formulas $F,F^{\prime}$ with $\mathit{env}_{F}(C)=\mathit{env}_{F^{\prime}}(C)$, it holds that $(F,C)\in\mathcal{P}$ if and only if $(F^{\prime},C)\in\mathcal{P}$.

The following is easily seen to hold:

Theorem 3**.**

$\mathsf{SEM_{BC}}$* is a local redundancy property.*

Preparatory for showing that $\mathsf{SEM_{BC}}$ is actually the most general local redundancy property (cf. Theorem LABEL:thm:semblocked_is_most_general below), we first prove the following lemma:

Lemma 4**.**

If a clause $C$ is not semantically blocked in a formula $F$, then there exists a formula $F^{\prime}$ with $\mathit{env}_{F^{\prime}}(C)=\mathit{env}_{F}(C)$ such that $C$ is not redundant with respect to $F^{\prime}$.