Minimization for Generalized Boolean Formulas

1 Introduction

The minimization problem for propositional formulas is one of the most natural optimization problems in the polynomial hierarchy. In fact, a variant of this problem was a major motivation for the definition of the polynomial hierarchy [Meyer and Stockmeyer, 1972]. The goal of minimization is to find a minimum equivalent formula to a given input formula. In this paper, we study the minimum equivalent expression (MEE) problem, where the input is a formula ϕ and a number k, and the question is to determine whether there exists a formula which is equivalent to ϕ and of size at most k (we study different notions of "size").

The problem is trivially in Σp2 , but a better lower bound than coNP-hardness had been open for many years. In [Hemaspaandra and Wechsung, 2002], the MEE problem was shown to be (many-one) hard for parallel access to NP. Recently, it was shown to be Σp2 -complete under Turing reductions in [Buchfuhrer and Umans, 2011].

Minimization in restricted fragments of propositional logic has been studied for the case of Horn formulas in order to

∗ Supported in part by NSF grants CCR-0311021 and IIS0713061, the DAAD postdoc program, and by a Friedrich Wilhelm Bessel Research Award. Work done in part while Henning Schnoor was at the Rochester Institute of Technology.

Henning Schnoor

Institute for Computer Science Christian-Albrechts-Universit¨at zu Kiel Kiel, Germany

find small representations of knowledge bases [Hammer and Kogan, 1995]. Prime implicates, a central tool for minimizing Boolean formulas [Quine, 1952], have been used in several areas of artificial intelligence research. We mention [Adjiman et al., 2006], where prime implicates were used in peer-to-peer data management systems for the semantic web, and [Bittencourt, 2008], which applies them in the context of belief change operators. Two-level logic minimization is an important problem in logic synthesis [Umans et al., 2006]. Different variants of minimization have been studied: The problem is Σp2 -complete for CNF formulas [Umans, 2001], NP-complete for Horn formulas [Boros and ˇCepek, 1994], and solvable in P for 2CNF formulas [Chang, 2004].

In this paper we study the complexity of minimization for syntactically restricted formulas. Two frameworks for restricting the expressive power of propositional logic have been used for complexity classifications in recent years:

• The Post framework [Post, 1941] considers formulas that instead of the usual operators ∧, ∨, and ¬, use an arbitrary set B of Boolean functions as connectors. Depending on B, the resulting formulas may express only a subset of all Boolean functions, or may be able to express all functions more succinctly than the usual set {∧, ∨, ¬}.
• The constraint framework [Schaefer, 1978] studies formulas in CNF, where the types of allowed clauses (e.g., Horn, 3CNF, or XOR clauses) are defined in a constraint language Γ containing "templates" of generalized CNFclauses that are allowed in so-called Γ-formulas.

In both frameworks, a wide range of complexity classifications has been obtained. For the Post framework, we mention the complexity of satisfiability [Lewis, 1979], equivalence [Reith, 2001], modal satisfiability [Hemaspaandra et al., 2010], and non-monotonic logics [Thomas and Vollmer, 2010]. In the constraint setting, besides the satisfiability problem [Schaefer, 1978; Allender et al., 2009], also enumeration of solutions [Creignou and H´ebrard, 1997], equivalence and isomorphism [B¨ohler et al., 2002], circumscription [Nordh and Jonsson, 2004], and many other problems have been studied, see [Creignou and Vollmer, 2008] for a survey. The complexity of satisfiability for non-Boolean domains is also a very active field, see e.g., [Bulatov, 2006; Bulatov and Valeriote, 2008].

For many considered problems, "dichotomy results" were achieved, proving that every choice of B or Γ leads to one of the same two complexity degrees, usually polynomial-time solvable and NP-complete. This is surprising since there are infinitely many sets B and Γ, and we know that there are, for example, infinitely many degrees of complexity between P and NP cases unless P = NP [Ladner, 1975].

A "Galois Connection" between constraint languages and closure properties in the Post setting determines the complexity of many computational problems [Jeavons et al., 1997; Schnoor and Schnoor, 2008]. In contrast, we show that these tools do not apply to minimization.

In the Post setting, we obtain a complete classification of the tractable cases of the minimization problem: For a set B of Boolean functions, the problem to minimize B-formulas is solvable in polynomial time or coNP-hard, hence avoiding the degrees between P and coNP-completeness. Our results in this framework apply to both the formula and the circuit case, and to different notions of size of formulas and circuits.

In the constraint case, we define irreducible constraint languages, among which we identify a large class whose formulas can be minimized in polynomial time, and prove NPor coNP-hardness results for most of the remaining cases. More precisely, we prove the following: For an irreducible language for which equivalence can be tested efficiently, minimization is NP-complete if the language can express (dual) positive Horn, and can be solved in polynomial time otherwise. Our analysis thus implies that the NP-completeness result for positive Horn shown in [Boros and ˇCepek, 1994] is "optimal:" As soon as a CNF fragment of propositional logic is strictly less expressive than positive Horn, formulas can be minimized efficiently. Since irreducibility is a natural condition for constraint languages that are used in knowledge representation, a consequence of our result is that knowledge bases that do not need the full expressive power of positive Horn admit efficient "compression algorithms."

Our contribution is threefold:

1. We give new and non-trivial minimization algorithms for large classes of formulas.
2. In the Post setting, we prove that all remaining cases are coNP-hard. In the constraint setting, we give strong evidence that larger classes do not have efficient minimization algorithms.
3. We show that minimization behaves very differently than many other problems in the context of propositional formulas: The usually-applied algebraic tools for the constraint setting cannot be applied to minimization. Also, complexities in the Post- and constraint framework differ strongly: In particular, the constraint framework contains NP-complete cases; such cases do not exist in the Post framework (unless NP = coNP).

Due to space restrictions, most proofs can only be found in the technical report [Hemaspaandra and Schnoor, 2011].

2 Minimization in the Post Framework

We fix a finite set B of finitary Boolean functions. We define B-formulas inductively: A variable x is a B-formula, and if ϕ1, . . . , ϕn are B-formulas, and f is an n-ary function from B, then f(ϕ1, . . . , ϕn) is a B-formula. We often identify the function f and the symbol representing it. VAR(ϕ) denotes the set of variables in a formula ϕ. We write ϕ(x1, . . . , xn) to indicate that VAR(ϕ) = {x1, . . . , xn}. For an assignment α : VAR(ϕ) → {0, 1}, the value of ϕ for α, ϕ(α), is defined in the straightforward way. We write α |= ϕ if ϕ(α) = 1, and say that α satisfies ϕ. Formulas ϕ1 and ϕ2 are equivalent if ϕ1(α) = ϕ2(α) for all α, we then write ϕ1 ≡ ϕ2. The satisfiability problem for B-formulas is denoted with SAT(B).

Formulas can be succinctly represented as circuits, which are essentially DAGs where formulas are trees. Although every circuit can be rewritten into a formula, the size of the resulting formula can be exponential in the size of the circuit.

In the Post framework, we study two variations of the minimization problem that differ in the notion of the size of a formula ϕ. An obvious way to measure size is the number of occurrences of literals, which we denote with sizel(ϕ). The second measurement is motivated by the study of Boolean circuits, where the size of a circuit is usually the number of non-input gates. For a formula, this is the number of appearing function symbols. We denote this number with sizes(ϕ). Our results also hold for obvious variations of these measures (e.g., counting variables instead of occurrences, also counting input gates, etc). For a set B as above, we define:

Problem: MEEF/C l/s (B)

Input: AB-formula/circuit φ and a number k

Question: Is there a B-formula/circuit ψ with

sizel/s(ψ) ≤ k and φ

≡

ψ?

An n-ary Boolean function f is an OR-function if it is constant or if f(x1, . . . , xn) is equivalent to xr1 ∨xr2 ∨· · ·∨xrm for a subset {xr1 , xr2 , . . . , xrm } ⊆ {x1, . . . , xn}. AND- and XOR-functions are defined analogously. We show that formulas using only these functions can be minimized easily:

Theorem 2.1 MEEF/C l/s (B) can be solved in polynomial time if B contains only OR-functions, only AND-functions, or only XOR-functions.

We mention that the theorem, as all of our results in this section, applies to all four combinations of F/C and s/l. We also stress that all algorithms in this paper do not only determine whether a formula with the given size restriction exists, but also compute a minimum equivalent formula.

The satisfiability problem for the above cases can easily be solved in polynomial time. We now show that this is indeed a prerequisite for a tractable minimization problem-formally, we prove that the complement of the satisfiability problem (i.e., the set of all binary strings that are not positive instances of SAT(B)) reduces to the minimization problem.

Theorem 2.2 For every finite set B of Boolean functions, SAT(B) ≤log m MEEF/C l/s (B).

Using results on the complexity of SAT(B) [Lewis, 1979], we obtain hardness results for a large class of sets B:

Corollary 2.3 Let B be a finite set of Boolean functions such that there is a B-formula that is equivalent to x ∧ y. Then MEEF/C l/s (B) is coNP-hard.

The remaining cases are those where satisfiability is tractable, but which are not of the forms covered by Theorem 2.1. We show that in these cases, minimization is coNPhard using a reduction from the equivalence problem for formulas, which asks to determine whether two given formulas are equivalent. The proof of the theorem below relies on the following idea: Given two formulas as input for the equivalence problem, we combine them into a single formula which is "trivial" if the formulas are equivalent, but "complicated" otherwise. The "gap" between the cases is large enough to yield a reduction to the minimization problem.

Theorem 2.4 MEEF/C l/s (B) is coNP-hard if one of the following is true:

• There is a B-formula equivalent to x∧y, and a B∪{1}- formula equivalent to x ∨ y,
• there is a B-formula equivalent to (x ∧ y) ∨ (x ∧ z) ∨ (y ∧ z).

Proof Sketch. We only handle the first case. Testing whether two B-formulas H1 and H2 are equivalent is coNP-hard ([Reith, 2001]). We reduce this problem to MEEF/C s (B). By assumption, there are B-formulas f∨(x, y, t) and f∧(x, y) with f∧(x, y) ≡ x∧y, and f∨(x, y, 1) ≡ x∨y. Let mbe the maximal arity of a function in B. For a new variable t, define

• l = sizes(f∧(H1, t)), we assume l > 1.
• Z is equivalent to ∧m·l i=1 zi for new variables zi.
• G = f∧(f∨(f∧(H1, H2), f∧(f∨(H1, H2, t), Z), t), t).

G can be computed in polynomial time using a logarithmic-depth tree construction. One can show that H1 ≡ H2 if and only if 〈G, l〉 ∈ MEEF/C s (B). The proof for MEEF/C l (B) uses a similar construction. □

Using algebraic techniques, the above implies that if B contains functions f, g, and h such that f that is not an ORfunction, g is not an AND-function, and h is not an XORfunction, then minimization is coNP-hard. This applies to all cases except those covered by our polynomial-time results. We therefore obtain the following full classification:

Corollary 2.5 Let B be a finite set of Boolean functions.

• If B contains onlyOR-functions, only AND-functions, or only XOR-functions, then MEEF/C l/s (B) can be solved in polynomial time.
• Otherwise, MEEF/C l/s (B) is coNP-hard.

3 Minimization in the CNF framework

Constraint formulas are CNF-formulas, where the set of allowed types of clauses is defined in a constraint language Γ, which is a finite set of non-empty finitary Boolean relations. A Γ-clause is of the form R(x1, . . . , xn), where R is an n-ary relation from Γ, and x1, . . . , xn are variables. A Γ-formula is a conjunction of Γ-clauses, it is satisfied by α, if for every clause R(x1, . . . , xn) in ϕ, we have that (α(x1), . . . , α(xn)) ∈ R. A relation R is expressed by a formula if the tuples in the relation are exactly the solutions of the formula (with some canonical order on the variables). We denote the satisfiability problem for Γ-formulas with SAT(Γ).

A natural way to measure the size of a CNF formula is the number of clauses-for a fixed language Γ, this is linearly related to the number of variable occurrences. We thus consider the following problem:

Problem: MEE(Γ)

Input: A Γ-formula ϕ, an integer k

Question: Is there a Γ-formula ψ with at most k ≡

clauses and ψ ϕ?

To state our classification, we recall relevant properties of Boolean relations (for more background on these properties and how they relate to complexity classifications of constraint-related problems, see e.g., [Creignou et al., 2001]).

1. A relation is affine if it can be expressed by a {x, x, x1 ⊕ · · · ⊕ xn, ¬(x1 ⊕ · · · ⊕ xn) | n ∈ N}-formula.
2. A relation is bijunctive if it can be expressed by a Γ2 - formula, where Γ2 is the set of binary Boolean relations.
3. A relation is Horn if it can be expressed by a {x, x, (x1 ∧ · · · ∧ xn → y), (x1 ∧ · · · ∧ xn) | n ∈ N}-formula.
4. A relation is positive Horn if it can be expressed by a {x1 ∧ · · · ∧ xn → y | n ∈ N}-formula.
5. A relation is IHSB+ if it can be expressed by a {x, x, x → y, (x1 ∨ · · · ∨ xn) | n ∈ N}-formula.

A constraint language Γ is affine, bijunctive, etc., if every relation in Γ is. Γ is dual (positive) Horn if Γ is (positive) Horn, and IHSB- if Γ is IHSB+. Here Γ is the dual of Γ, obtained from Γ by swapping 0 and 1 in all relations in Γ. Additionally, Γ is Schaefer if it is affine, bijunctive, Horn, or dual Horn. This property implies tractability of many problems for Boolean constraint languages, including satisfiability [Schaefer, 1978], equivalence [B¨ohler et al., 2002] and enumeration [Creignou and H´ebrard, 1997].

3.1 Irreducible Relations

In many cases, if constraint languages Γ1 and Γ2 "have the same expressive power," then problems for Γ1 and Γ2 have the same complexity. We show that this is not true for minimization, even for a very strict version of "having the same expressive power" (see [Schnoor and Schnoor, 2008] for details on notions of expressive power).

Example 3.1 Let Γ1 := {x ∨ y} and Γ2 := {(x ∨ y), (x ∨ (y ∧ z)), (x ∨ (y ∧ z ∧ w))}.

• Γ1 and Γ2 have the same expressive power, since y ∨ (x1 ∧ · · · ∧ xn) ≡ (y ∨ x1) ∧ · · · ∧ (y ∨ xn).
• MEE (Γ1) can be solved in polynomial time.
• MEE (Γ2) is NP-hard by a reduction from Vertex Cover for cubic graphs: A cubic graph G = (V, E) has a vertex cover of size k if and only if the formula ∧{i,j}∈E (xi ∨
• xj) has an equivalent Γ2-formula with k clauses.

Hence unlike most problems in the constraint context, the complexity of minimization is not determined by the expressive power of a constraint language. This is the reason why our analysis cannot simply follow the well-established line of reasoning used to obtain complexity classifications in the literature. Considering the above example, the problems in minimizing Γ2-formulas are combinatorial and do not stem from the difficulty of determining a "minimum representation" of a given formula. Therefore the NP-hardness is not in finding a minimum representation of the formula, but from the difficulty to use the available "building blocks" efficiently.

In the example above, the problems arise because Γ2 contains "combined" relations which can be rewritten into simpler clauses: (x ∨ (y ∧ z)) is equivalent to (x ∨ y) ∧ (x ∨ z). An important feature of constraint formulas is that they build formulas from "local conditions" expressed in the individual clauses. The clause (x ∨ (y ∧ z)) is in a way not "as local as it can be," since it can be rewritten as the conjunction of two "easier" conditions. We define irreducible relations as those that cannot be rewritten in this way:

Definition An n-ary relation R is irreducible, if for every formula R1(x11 . . . , x1k1 ) ∧ · · · ∧ Rm(xm1 , . . . , xmkm ) (where each Ri is a ki-ary Boolean relation) which is equivalent to R(x1, . . . , xn), one of the Ri-clauses has arity at least n. A constraint language Γ is irreducible if every relation in Γ is.

Irreducibility is a rather natural condition-in fact, most relations usually considered in the constraint context meet this definition. Irreducible languages only allow "atomic" clauses that cannot be split up further. In practice, for example in the design of knowledge bases, irreducible languages are more likely to be used: They provide users with atomic constructs as a basis from which more complex expressions can be built.

3.2 Polynomial-Time Cases

We prove polynomial-time results for every case in which such a result is conceivable: The MEE problem for positive Horn formulas is NP-complete [Boros and ˇCepek, 1994]. We show that for every irreducible constraint language that is Schaefer, and does not have all the expressive power of positive Horn (or dual positive Horn), the minimization problem can be solved efficiently. For non-Schaefer languages, even testing equivalence is coNP-hard, and hence an efficient minimization procedure cannot be expected. Following known structural results about Boolean constraint languages, there are three cases to consider: The case where Γ is affine, bijunctive, or IHSB+. We provide polynomial-time algorithms for all of these cases.

IHSB+ and IHSB- formulas

We start our polynomial-time results with the most involved of these constructions, proving that irreducible constraint languages that are IHSB+ lead to an easy minimization problem (the IHSB- case is analogous). Requiring irreducibility is necessary: The language Γ2 discussed in Example 3.1 is IHSB+ (even considerably less expressive than IHSB+), but, as argued before, has an NP-hard minimization problem.

The main idea of the algorithm is the following: We rewrite formulas using multi-ary OR, implication, equality, and literals into conjunctions of, to a large degree, independent formulas, each containing only OR, implications, equalities, or literals. Each of these formulas then can be minimized locally with relatively easy algorithms. The main task that our algorithm performs is "separating" the components of the input formula in such a way that minimizing the mentioned subformulas locally is equivalent to minimizing the entire formula.

Proof. For variables u and v, we write u ⇝ϕ v (u leads to v in ϕ) if there is a directed {→, =}-path in ϕ from u to v, we often simply write u ⇝ v. Similarly, if there are OR-clauses C1 = (x1 ∨ · · · ∨ xn) and C2 = (y1 ∨ · · · ∨ ym), we write C1 ⇝ C2 if every of the xi leads to one of the yj. Since satisfiability for Γ-formulas can be tested in polynomial time, we assume that all occurring formulas are satisfiable. For any Γ-formula ϕ, let ϕOR denote the formula obtained from ϕ by removing every clause that is not an OR-clause with at least 2 variables, and let ϕ→ be the conjunction of all implicationclauses in ϕ, ϕlit the literals in ϕ, and ϕ= the equality clauses.

We now describe the minimization procedure. We use some canonical way of ordering variables and clauses and repeat the following steps until no changes occur anymore:

• 1: Input: Γ-formula ϕ
• 2: while changes still occur do
• 3: For a set of variables connected with =, only keep the minimal variable in non-equality clauses (by variable identification)
• 4: if there exist OR-clauses C1 ̸= C2 with C1 ⇝ C2, then
• 5: If C2 ⇝ C1, then remove the minimal of the two
• 6: Otherwise, remove C2
• 7: end if
• 8: if there is clause (x1 ∨· · ·∨xn), variable v with xi ⇝ v for all i, then
• 9: introduce clause v 10: remove →-clauses leading to v

11: end if

12:

13:

• if literal x occurs, x ⇝ y then replace final clause in path with y

14: end if

15:

if literal y occurs, x ⇝ y then

16:

replace first clause in path with x

17: end if

• 18: Remove variables occurring as negative literals from OR-clauses

19:

20:

• if (x1 ∨ · · · ∨ xn) is clause, xi ⇝ xj for i ̸= j then remove xi from the clause
• 21: end if

22:

• if there are variables such that x1 ⇝ x2, . . . , xn-1 ⇝ xn, xn ⇝ x1 then
• 23: exchange implications between them with equalities.
• 24: end if
• 25: if u (u) appears as a literal then
• 26: remove clauses of the form (v → u) ((u → v)).
• 27: end if
• 28: Locally minimize ϕ= and ϕ→.
• 29: end while

Note that ϕ= and ϕlit can be minimized trivially, and ϕ→ can be minimized due to a result from [Aho et al., 1972], since finding a transitive reduction of a directed graph is exactly the problem of minimizing a formula in which only implications of positive literals appear. It can be shown that the algorithm produces a formula that is equivalent to the input and minimal with respect to the number of clauses. □

A careful analysis of the proof yields that it also holds true if Γ does not contain all the relations defining IHSB+, even though in these cases, only a restricted vocabulary is available for the minimum formula, and also applies in the cases where the relations are not the ones mentioned in the theorem, but are still IHSB+ (the IHSB- case is analogous):

Corollary 3.3 Let Γ be an irreducible constraint language which is IHSB+ or IHSB-. Then MEE (Γ) ∈ P.

We mention that the above cases remain polynomial-time if the input formula may use clauses of unbounded arity.

Bijunctive Formulas

In a similar way, we show that irreducible bijunctive constraint languages give a tractable minimization problem:

Theorem 3.4 Let Γ be a constraint language which is irreducible and bijunctive. Then MEE (Γ) ∈ P.

Affine Formulas

We conclude our polynomial-time results with the affine case. Affine formulas represent linear equations over GF (2). We therefore can apply standard linear algebra techniques to obtain an efficient minimization algorithm.

Theorem 3.5 Let Γ be an irreducible and affine constraint language. Then MEE (Γ) ∈ P.

3.3 Lower Bounds

As mentioned before, our polynomial-time results cover all cases where polynomial-time algorithms can be expected. We now prove hardness results for most of the remaining cases.

Minimization and Satisfiability

If a constraint language Γ is not Schaefer (i.e., neither Horn, dual Horn, bijunctive, nor affine), then the satisfiability problem for Γ+ = Γ ∪ {x, x} (Γ extended with literals) is NPcomplete. Since the natural analog of Theorem 2.2 can also be shown in the CNF setting, we obtain the following:

Corollary 3.6 Let Γ be a constraint language that is not Schaefer. Then MEE(Γ+) is coNP-hard.

NP-completeness Results

We use results on the hardness of minimizing Horn formulas to obtain an NP-completeness result for a large class of constraint languages: An irreducible constraint language that is not covered by our polynomial-time results, but that is Schaefer, leads to an NP-complete minimization problem. The NP upper bound is clear, since the equivalence problem can be solved in polynomial time in these cases. The proof of the hardness result is more involved, and first establishes a characterization of the relations contained in the covered constraint languages, which shows that in all cases, we have a relation that is expressive enough to encode minimization for positive Horn formulas. We thus obtain the following result:

Theorem 3.7 Let Γ be an irreducible constraint language that is Schaefer, not affine, not bijunctive, not IHSB+, and not IHSB-. Then MEE (Γ) is NP-complete.

3.4 Classification Theorem

The analysis in the previous sections yields the following classification:

Theorem 3.8 Let Γ be an irreducible constraint language.

1. If Γ is affine, bijunctive, IHSB+, or IHSB-, then MEE (Γ) ∈ P.
2. Otherwise, if Γ is Horn or dual Horn, then MEE(Γ) is NP-complete,
3. Otherwise, Γ is not Schaefer, and MEE(Γ+) is coNPhard.

While the theorem does not completely classify the complexity of the MEE problem for all irreducible constraint languages, we consider it unlikely that there exist more polynomial-time cases than the ones we discovered: To the best of our knowledge, no decision problem for non-Schaefer languages has been proven to be in polynomial time except for trivial cases (e.g., satisfiability is trivial if all relevant relations contain the all-0 tuple). Also, for non-Schaefer languages Γ, already testing equivalence of formulas is coNPhard. This implies that, unless P = NP, there cannot be a polynomial-time algorithm that, given a Γ-formula, computes its "canonical" (i.e., up to differences checkable by a polynomial-time algorithm) minimum equivalent expression. We are therefore confident that our classification covers all polynomial-time cases for irreducible constraint languages.

It is worth noting that the prerequisite that Γ is irreducible is certainly required for the polynomial-time cases, as the earlier example highlighted. For the hardness results, this is less clear-the coNP-hardness does not rely on this prerequisite at all, and for the NP-complete Horn cases, we consider it unlikely that there is a constraint language with the same expressive power that does not directly encode positive Horn.

4 Conclusion and Open Questions

We studied the complexity of minimization for restricted classes of propositional formulas in two settings, obtained a complete characterization of all tractable cases in the Post case, and a large class of tractable cases in the constraint case.

Open questions include the exact classification of the coNP-hard cases. It is likely that most of them are NP-hard as well. It would be very interesting to determine whether some of these are actually Σp2 -complete (this does not follow directly from the Σp2 -completeness of the minimization problem for CNF formulas [Umans, 2001], since our constraint languages Γ and bases B are finite). Finally, non-irreducible constraint languages are an interesting open issue.

Acknowledgment

We thank the anonymous reviewers for many helpful comments, in particular for pointing out an issue with the definition of irreducibility.