Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood?

1 Introduction

Every once in a while, you hear about neighbors who are just not the kind of neighbors you would wish for. For instance, the grumpy dude next door who starts mowing his lawn on an early Sunday morning while you are still lying in bed. Or, the student in the apartment below yours, who regularly decides around midnight that nowmight be the perfect time for listening to some not so calm rock music. Whatever it is that makes them such pleasant neighbors, in case they decide to leave your neighborhood, you rarely find anyone shedding tears over their departure.

In this paper, we show that bad neighbors also play a significant role in modern SAT solving. They might not rob you of your well-earned sleep, but-rather subtly-they present themselves in the form of locally redundant clauses. Here, redundant means that we can remove these clauses from a formula in conjunctive normal form without causing any sorrow, i.e., without affecting the formula's satisfiability. Local means that we do not need to consider the whole formula to find out that these clauses are redundant-it suffices to consider only their resolution neighborhood, i.e., the set of clauses they can be resolved with.

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

Hans Tompits TU Wien, Austria tompits@kr.tuwien.ac.at Armin Biere JKU Linz, Austria biere@jku.at

Among the types of locally redundant clauses, blocked clauses [Kullmann, 1999] are of particular interest. 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 are tautologies. The elimination of blocked clauses can significantly boost the performance of SAT solvers [Manthey et al., 2013; J¨arvisalo et al., 2010]. Moreover, blocked clauses yield the basis for blocked-clause decomposition [Heule and Biere, 2013], a technique that splits a formula into two parts that become solvable by blocked-clause elimination. Blockedclause decomposition is successfully used for gate extraction, for efficiently finding backbone variables, and for the detection of implied binary equivalences [Iser et al., 2015; Balyo et al., 2014]. The winner of the SATRace 2015 competition, abcdSAT [Chen, 2015], uses blocked-clause decomposition as core technology.

These success stories provide the motivation for having a closer look at locally redundant clauses in general, and at blocked clauses in particular. In this paper, we discuss powerful generalizations of blocked clauses that are still locally redundant: set-blocked clauses and super-blocked clauses. The latter kind of clauses actually constitutes the most general concept of a locally redundant clause. Rounding off the picture, we furthermore discuss the complexity of deciding whether a clause is set-blocked or super-blocked.

The rest of this paper is structured as follows. After introducing the necessary preliminaries in Section 2, we recapitulate popular kinds of locally redundant clauses in Section 3. Afterwards, Section 4 contains our discussion of set-blocked clauses and super-blocked clauses, and Section 5 contains complexity results related to checking these redundancy notions. Section 6 concludes our paper with an outlook on future work.

This paper is an abridged version of a paper that appeared in the proceedings of IJCAR 2016, the Eight International Joint Conference on Automated Reasoning [Kiesl et al., 2016].

2 Preliminaries

We consider propositional formulas in conjunctive normal form (CNF), which are defined as follows. A literal is either a variable x (a positive literal) or the negation ¬x of a variable x (a negative literal). For a literal l, we define its complement ¯l as ¬x if l = x and as x if l = ¬x. Accordingly, for a set L of literals, we define ¯L = {¯l | l ∈ L}. A clause is a disjunction of literals. A formula in CNF 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 ¯l for some literal l. For a literal, clause, or formula F, var(F) denotes the set of variables occurring in F. For convenience, we often treat var(F) as a variable if F is a literal. For a set L of literals and a formula F , we denote by FL the set of all clauses in F that contain a literal of L, i.e., FL = {C | C ∈ F, C ∩ L ̸= ∅}. In case L is a singleton set of the form {l}, we sometimes write Fl instead of F{l}.

An assignment is a partial function from a set of variables to the truth values 1 (true) and 0 (false). Given an assignment α and a literal l, αl is the assignment obtained from α by flipping the truth value of l, i.e., αl(v) = 1 - α(v) if v = var(l) and αl(v) = α(v) otherwise. A literal l is satisfied by an assignment α if l is positive and α(var(l)) = 1 or if it is negative and α(var(l)) = 0. A clause is satisfied by an assignment α if it contains a literal that is satisfied by α. Finally, a formula is satisfied by an assignment α if all of its clauses are satisfied by α. A formula is satisfiable if there exists an assignment that satisfies it. Two formulas are logically equivalent if they are satisfied by the same assignments. Two formulas F and F ′ are satisfiability equivalent if F is satisfiable if and only if F ′ is satisfiable.

Given two clauses C and D together with a literal l ∈ C such that ¯l ∈ D, the clause (C \ {l}) ∪ (D \ {¯l}) is called the resolvent of C and D upon l. Given a formula F and a clause C, the resolution neighborhood, RNF (C), of C in F is the set of all clauses in F that can be resolved with C:

The variables in var(C) are called local variables and the variables in var(RNF (C)) \ var(C) are the external variables, denoted by extF (C).

Next, we recapitulate the formal notion of clause redundancy [Kiesl et al., 2016]. Intuitively, a clause C is redundant w.r.t. a formula F if neither its addition to F nor its removal from F changes the satisfiability or unsatisfiability of F .

Definition 1 A clause C is redundant w.r.t. a formula F if the formulas F \ {C} and F ∪ {C} are satisfiability equivalent. A redundancy property is a set of pairs (F,C) where C is redundant w.r.t. F . Finally, for two redundancy properties P1 and P2, P1 is more general than P2 if P2 ⊆ P1. Accordingly, P1 is strictly more general than P2 if P2 ⊂ P1.

Consider, for example, the formula F = {(a∨b), (¬a∨¬b)}. The clause C = (¬a ∨¬b) is redundant w.r.t. F since the formulas F \ {C} and F ∪ {C} are satisfiability equivalent (although they are not logically equivalent). Moreover, the set {(F, C) | F is a formula and C is a tautology} is a redundancy property since for every formula F and every tautology C, F \ {C} is satisfiability equivalent to F ∪ {C}.

Note that C is not redundant w.r.t. F if and only if F \{C} is satisfiable and F ∪ {C} is unsatisfiable. To prove that C is redundant w.r.t. F, it therefore suffices to show that the satisfiability of F \{C} implies that of F ∪{C}. Redundancy properties as defined above yield not only the basis for clauseelimination but also for clause-addition procedures [J¨arvisalo et al., 2012].

3 Local Redundancy Properties

In this section, we discuss some well-known redundancy properties from the literature to motivate the definition of socalled local redundancy properties. The simplest example of a redundant clause is a tautology. As every assignment satisfies exactly one of the two complementary literals contained in a tautology, tautologies are always true and therefore redundant w.r.t. every formula. Because of this, the set {(F,C) | F is a formula and C is a tautology} is a redundancy property. To decide whether a clause is a tautology w.r.t. a formula F , we only need to look at C itself.

Another example for redundant clauses are so-called clauses with pure literals [Davis and Putnam, 1960]. A literal is pure in a formula if its complementary literal does not occur in the formula. In contrast to tautologies, clauses with pure literals are not guaranteed to be satisfied by every assignment. Still, we can easily see that they are redundant: Let C be a clause containing a literal l that is pure in a formula F and assume we have some assignment α that satisfies F \ {C} but falsifies C. We can then turn α into a satisfying assignment αl of F ∪ {C} by flipping the truth value of l. None of the clauses in F \ {C} can be falsified by this since they do not contain the literal ¯l, which is the only literal whose truth value is negatively affected by setting l to true. The corresponding redundancy property is the set {(F,C) | C contains a literal that is pure in F}.

The redundancy of a clause with pure literals is based on the fact that we can make one of its literals true without falsifying other clauses. In the case of pure literals, this is guaranteed since there are no clauses that contain the complementary literal. The more general blocked clauses [Kullmann, 1999] guarantee redundancy even in cases where other clauses might contain the complementary literal:

Definition 2 A clause C is blocked by a literal l ∈ C in a formula F if, for each clause D ∈ F¯l, C ∪ (D \ {¯l}) is a tautology.

We say that a clause is blocked in F if one of its literals blocks it in F . The following is an example of a blocked clause:

Example 1 Consider the clause C = (a∨b) and the formula F = {(¬a ∨ c), (¬b ∨ ¬a)}. The literal b blocks C in F since the only clause in F that contains ¬b is the clause D = (¬b ∨ ¬a), and C ∪ (D \ {¯l}) = (a ∨ b ∨ ¬a) is a tautology.

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 α satisfies F \ {C} but falsifies C. Like with pure literals, we can then easily turn α into a satisfying assignment αl of C by flipping the truth value of l. This flipping could possibly falsify some of the clauses in F \ {C} that contain ¯l, but the condition that l blocks C guarantees that these clauses stay satisfied: Let D be such a clause that contains ¯l. Then, since C ∪ (D \ {¯l}) is a tautology, either D is itself a tautology (and therefore trivially satisfied) or it contains a literal l′ ̸= l such that ¯l′ ∈ C. In the latter case, since α falsifies C, it must satisfy l′ and since αl agrees with α on all literals but l, αl is a satisfying assignment of F ∪ {C}. Hence, C is redundant w.r.t. F. We illustrate this argument on a concrete example:

Figure 1: The clause (a ∨ b) from Example 3 and its resolution neighborhood.

Example 2 Consider again the clause C = (a ∨ b) and the formula F = {(¬a ∨ c), (¬b ∨ ¬a)} from Example 1. We already know that b blocks C in F. Now, let α denote the assignment that falsifies the variables a, b, and c. Clearly, α satisfies F but falsifies C. We would expect that the assignment αb, obtained from α by flipping the truth value of b, satisfies not only C but also all clauses of F. This is indeed the case. The only clause that could have been falsified by flipping the truth value of b is the clause D = (¬b ∨¬a). But D stays true since αb satisfies ¬a, which is not a coincidence: C ∪ (D \ {¬b}) is a tautology and must therefore be satisfied by αb. Moreover, we know that α falsifies C. Therefore, αb must satisfy D \ {¬b} = (¬a).

A closer look at blocked clauses reveals two things. First, the redundancy property of blocked clauses (i.e., the set {(F, C) | C is blocked in F}) is more general than the redundancy properties of tautologies and pure literals. If a clause C is a tautology, then C ∪ (D \ {l}) is a tautology for every D, implying that C is blocked. If C contains a literal that is pure in a formula F, then F¯l = ∅ and thus it vacuously holds that C ∪ (D \ {l}) is a tautology for all D ∈ F¯l. Therefore, tautologies and clauses with pure literals are blocked clauses.

Second, to detect whether a clause C is blocked in a formula F, it suffices to consider only those clauses of F that contain a literal ¯l such that l ∈ C, i.e., the clauses in RNF (C). The question arises whether there exist redundant clauses that are not blocked but whose redundancy can be identified by considering only their resolution neighborhood. As shown in the next example, this is indeed the case:

Example 3 Consider C = (a ∨ b) and let F be a formula such that RNF (C) = {(x∨b∨¬a), (¬b∨¬x), (¬b∨a)} (cf. Figure 1). Clause C is not blocked in F but redundant: Suppose there exists an assignment α that satisfies F but falsifies C. Then, α must satisfy either x or ¬x. If α(x) = 1, then C can be satisfied by flipping the truth value of a, resulting in assignment α′ = αa. Since α′ (x) = 1, the clause (x∨b∨¬a) stays satisfied. In contrast, if α(x) = 0, we can satisfy C by the assignment α′′ , obtained from α by flipping the truth values of both a and b: The fact that α′′ (b) = 1 guarantees that (x ∨ b ∨ ¬a) stays satisfied whereas α′′ (x) = 0 and α′′ (a) = 1 guarantee that both (¬b ∨ ¬x) and (¬b ∨ a) stay satisfied. Since flipping the truth values of literals in C does not affect the truth of clauses outside the resolution neighborhood RNF (C) of C, we obtain in both cases a satisfying assignment of F .

If a clause C is redundant w.r.t. a formula F and this redundancy can be identified by considering only its resolution neighborhood in F, then C is redundant w.r.t. every formula F ′ in which it has the same resolution neighborhood as in F. Such a redundancy is called local [Kiesl et al., 2016]:

Definition 3 A redundancy property P is local if, for every clause C and any two formulas F, F ′ with RNF (C) = RNF ′(C), it holds that either {(F,C), (F ′ ,C)} ⊆ P or {(F, C), (F ′ , C)} ∩ P = ∅.

In the next section, we present redundancy properties that are strictly more general than blocked clauses while still being local.

4 Set-Blocking and Super-Blocking

We now turn our attention to the local redundancy properties of set-blocked clauses and super-blocked clauses [Kiesl et al., 2016]. Both strictly generalize blocked clauses. Superblocked clauses even constitute the most general local redundancy property. The idea behind set-blocked clauses is to allow for flipping the truth values of more than one literal:

Definition 4 Let F be a formula and C a clause. A nonempty set L ⊆ C blocks C in F if, for each clause D ∈ F¯L, (C \ L) ∪ ¯L ∪ D is a tautology.

We say that a clause is set-blocked in F if there exists a set that blocks it in F. Moreover, we write SET for the set {(F, C) | C is set-blocked in F}.

Example 4 Let C = (a ∨ b) and F = {(¬a ∨ b), (¬b ∨ a)}. Then, C is set-blocked by L = {a, b}: Clearly, F¯L = F and C \ L = ∅. Therefore, for D1 = (¬a ∨ b) we get that (C \ L) ∪ ¯L ∪ D1 = (a ∨ b ∨ ¬a) is a tautology and for D2 = (¬b ∨ a) we get that (C \ L) ∪ ¯L ∪ D2 = (a ∨ b ∨ ¬b) is a tautology as well. Note that C is not blocked in F .

Given an assignment α that satisfies F \ {C} but falsifies C, the existence of a blocking set L guarantees that we can turn α into a satisfying assignment αL of F ∪ {C} by flipping the truth values of all the literals in L. Since (C \ L) ∪ ¯L ∪ D is a tautology for every D ∈ F¯L, at least one of the following holds: (i) D is itself a tautology and thus satisfied by αL, or (ii) D contains a literal of L which is satisfied by αL since its truth value is flipped, or (iii) D contains a literal l which is satisfied since ¯l ∈ C is falsified by α and the truth value of l is not flipped. Hence, αL satisfies F ∪{C} and thus set-blocked clauses are redundant.

In order for a clause to be set-blocked, it is required that every assignment that satisfies F \ {C} but falsifies C can be turned into a satisfying assignment of F \ {C} by flipping the truth values of the literals in the blocking set L. This involves some inflexibility as we are not allowed to choose different blocking sets for different assignments. Consider the following example:

Example 5 Let C = (a∨b) and F = {(¬a∨x), (¬b∨¬x)}. The clause C is not set-blocked in F but redundant w.r.t. F. Suppose an assignment α satisfies F but falsifies C. We can easily turn α into a satisfying assignment of F ∪ {C}: If α satisfies x, flip the truth value of a. If α falsifies x, flip the truth value of b. In both cases, all clauses in F stay satisfied.

We obtain a more general redundancy property if we allow blocking sets to depend on the assignment at hand. In particular, on the assignment over the external variables. This gives rise to the notion of super-blocking. In the following, for a formula F and an assignment α, we denote by F|α the set of clauses obtained from F by removing all clauses that are satisfied by α. Recall that the external variables, extF (C), are the variables that are contained in RNF (C) but not in C.

Definition 5 A clause C is super-blocked in a formula F if, for every assignment τ over the variables in extF (C), C is set-blocked in F |τ .

We write SUP for the set {(F, C) | C is super-blocked in F}. For instance, the clause C in Example 5 is not set-blocked but super-blocked in F since it is set-blocked in F |α and F |α′ for α(x) = 1 and α′ (x) = 0. Likewise for the clause C and the corresponding formula F in Example 3. By removing the clauses that are satisfied by a certain assignment, we use the fact that the truth of clauses in the resolution neighborhood cannot only be established by literals whose variables occur in C, but also by the truth of literals over the external variables. Finally, note that if a clause is set-blocked in F, then it is also set-blocked in every F ′ ⊆ F and thus in every F |α. Hence we get:

Proposition 1 Super-blocking is strictly more general than set-blocking, i.e., it holds that SET ⊂ SUP.

One can show that super-blocked clauses constitute the most general local redundancy property [Kiesl et al., 2016]:

Theorem 2 The set SUP is the most general local redundancy property.

5 Complexity Results

In this section, we discuss complexity results for deciding whether a clause is set-blocked or super-blocked. We furthermore consider the complexity of deciding restricted variants of set-blocking and super-blocking that are obtained by bounding the size of blocking sets. As the redundancy properties of set-blocked clauses and super-blocked clauses are local, we consider only a clause and its resolution neighborhood as input to the corresponding decision problems.

Formally, the set-blocking problem is the following decision problem: Given a clause C and a formula F such that every D ∈ F contains a literal ¯l with l ∈ C, decide whether C is set-blocked in F . The super-blocking problem is defined analogously.

Clearly, the set-blocking problem is in NP: For a nonempty literal set L ⊆ C, we can check in polynomial time whether it blocks C in F-we just have to iterate over all clauses in F¯L and check whether (C \ L) ∪ ¯L ∪ D is a tautology. The following is thus an NP-procedure for deciding set-blockedness: Guess a non-empty set L ⊆ C and check if it blocks C in F. Hardness for the complexity class NP can be shown via a reduction from the satisfiability problem of propositional logic. The set-blocking problem is thus NPcomplete.

Deciding whether a clause is super-blocked is harder: Membership and hardness for ΠP2 can respectively be shown by an encoding to and a reduction from 2-QBF (∀∃-SAT). The intuition behind this is that super-blocking is "for-allexists" in nature-a clause C is super-blocked in a formula F if for all assignments α over the external variables, there exists a non-empty set L ⊆ C of literals such that C is setblocked in F |α.

Although the set-blocking problem is NP-complete in the general case, we can obtain a restricted variant of setblocking by only allowing blocking sets whose cardinalities are bounded by a constant. Then, the resulting problem of testing whether a clause C is blocked by some non-empty set L ⊆ C, whose size is at most k for k ∈ N+, turns out to be polynomial: For a finite set C and k ∈ N+, there are only polynomially many non-empty subsets L ⊆ C with |L| ≤ k. To see this, observe (by basic combinatorics) that the exact number of such subsets is given by the sum ∑ki=1 (|C| i ), which reduces to a polynomial with degree at most k.

Hence, the number of non-empty subsets L ⊆ C with |L| ≤ k is polynomial in the size of C. To decide whether a clause is set-blocked by a set of size at most k we thus just have to iterate over polynomially many candidate sets and check, in polynomial time, whether they block C. Likewise, bounding the size of the blocking sets in the definition of super-blocked clauses by a constant makes the corresponding decision problem simpler: Deciding super-blocking for bounded blocking sets is co-NP-complete.

The complexity results are summarized in Table 1 (from [Kiesl et al., 2016]). Note that the cardinality |L| of blocking sets is of course bounded by the length of the clauses. This is particularly interesting for formula instances with (uniform) constant or maximal clause length.

6 Conclusion

We discussed local redundancy properties and considered setblocked clauses and super-blocked clauses, which generalize blocked clauses while still being locally redundant, meaning that their redundancy can be identified by considering only their resolution neighborhood. In fact, super-blocked clauses constitute the most general local redundancy property. Deciding whether a clause is set-blocked is NP-complete and deciding whether a clause is super-blocked is ΠP2 -complete. Bounding the size of the blocking sets by a constant makes the corresponding decision problems go down one level in the polynomial hierarchy. The locality of redundancy properties is particularly interesting when dealing with formulas in which the resolution neighborhoods of clauses are small compared to the size of the whole formula. Concerning future work, we plan to implement clause-elimination techniques based on set-blocked clauses and super-blocked clauses. Moreover, we want to investigate whether these notions can be lifted to the level of quantified Boolean formulas.