On Minimum Representations of Matched Formulas (Extended Abstract)

1 Introduction

In this paper we study the class of matched formulas introduced in [Franco and Van Gelder, 2003]. Given a CNF formula ϕ we consider its incidence graph I(ϕ) defined as follows. I(ϕ) is a bipartite graph with one part consisting of clauses of ϕ and the other part containing the variables of ϕ. An edge {C, x} for a clause C and variable x is in I(ϕ) if x appears in C. It was observed in [Aharoni and Linial, 1986; Tovey, 1984] that if I(ϕ) admits a matching (i.e. a set of pairwise disjoint edges) of size m (where m is the number of clauses in ϕ), then ϕ is satisfiable. Later in [Franco and Van Gelder, 2003] the formulas satisfying this condition were called matched formulas. Since a matching of maximum size in a given graph can be found in polynomial time (see e.g. [Lov´asz and Plummer, 1986]), we can check whether a given formula is matched. Given an arbitrary CNF ϕ we can measure how far it is from being matched by considering its maximum deficiency δ∗ (ϕ), the number of clauses which remain unmatched in a maximum matching of I(ϕ). A formula ϕ is thus matched iff δ∗ (ϕ) = 0. A weaker notion of deficiency δ(ϕ) = m- n (where m is the number of clauses and n the number of variables in ϕ) is also often being considered.

Since their introduction, matched formulas were considered as a base class in parameterized algorithms for satisfiability (see e.g. [Flum and Grohe, 2006] for an overview of parameterized algorithms theory). In particular, the authors of [Fleischner et al., 2002] show that satisfiability of the formulas whose maximum deficiency is bounded by a constant can be decided in polynomial time. This result was later improved in [Szeider, 2003] to a an algorithm for satisfiability parameterized with maximum deficiency of a formula. Parameterization based on backdoor sets with respect to matched formulas were considered in [Szeider, 2007].

∗This paper is an updated extended abstract of an article in the Journal of Artificial Intelligence Research [ ˇCepek et al., 2014].

Several generalizations of matched formulas were considered in the literature, too. In [Kullmann, 2000], matched formulas were generalized into the class of linearly satisfiable formulas. Autarkies based on matchings were studied in [Kullmann, 2003]. Another generalization was considered in [Szeider, 2005] as classes of bi-clique satisfiable and varsatisfiable formulas. Unfortunately, for both bi-clique and var-satisfiable formulas it is hard to check if a formula falls into one of these classes [Szeider, 2005].

The results listed in the previous paragraphs show that matched formulas play a significant role in the theory of satisfiability solving which is, without any doubt, one of the most studied problems in theoretical computer science that has many practical applications. Despite this fact, little is known about the structure of matched CNFs. It is not hard to come up with examples of matched CNFs such that logically equivalent prime CNFs are not matched. This is quite a surprising phenomenon which does not occur in most classes with polynomial time satisfiability testing such as quadratic CNFs, Horn CNFs, and their various generalizations, for which once a CNF is in the class, all logically equivalent prime CNFs are guaranteed to be in the class as well. This brings an interesting question: given a (nonprime) matched CNF does there exist at least one equivalent prime CNF which is also matched? In this paper we give an affirmative answer to this question, and then use this fact to prove a stronger result: if a Boolean function f admits a representation by a matched CNF then every clause minimum CNF representation of f is matched. This is the main result of the current paper.

Another problem we study in this paper is Boolean minimization of matched CNFs. Boolean minimization problem (BM) can be stated as follows: given a CNF find a logically equivalent CNF with a minimum possible number of clauses. This natural optimization version can be turned into a decision version by adding a number k and asking whether there exists a logically equivalent CNF with at most k clauses. The decision version of BM was shown to be Σp2 - complete [Umans, 2001] for general CNFs (where Σp2 denotes the second level of polynomial hierarchy). It is also long known that for some classes of CNFs where SAT is solvable in polynomial time, BM is Σp1 -complete (where Σp1 denotes the first level of polynomial hierarchy which is better known as class NP), i.e. easier than in the general case. Maybe the best known example is the class of Horn CNFs (a CNF is Horn if every clause in it contains at most one positive literal). NP-completeness of BM for Horn CNFs was proved independently in several papers [Ausiello et al., 1986; ˇCepek, 1995; Hammer and Kogan, 1993; Maier, 1980; Boros et al., 2013]. For some classes of CNFs BM is even easier: there exists a hierarchy of tractable subclasses of Horn CNFs for which there are polynomial time minimization algorithms, namely acyclic and quasi-acyclic Horn CNFs [Hammer and Kogan, 1995], and CQ Horn CNFs [Boros et al., 2009]. There are also few heuristic minimization algorithms for Horn CNFs [Boros et al., 1998].

The complexity of BM for matched CNFs does not fit the above picture. Despite the fact that SAT is trivial for matched CNFs, BM for this class is Σp2 -complete, i.e. as hard as for the general case. This fact was proved in [Gursk´y, 2011], where the proof modifies the proof for the general case from [Umans, 2001]. In this paper we give a much simpler proof of the same fact which is based on an observation, that equivalence testing is co-NP-complete for matched CNFs.

2 Preliminaries

In this section we shall give the necessary definitions and recall several results we shall use in this paper.

2.1 Boolean Functions

An n-variable Boolean function is a mapping f : {0, 1}n → {0, 1}. A literal is either a variable or its negation. A clause is a disjunction of literals. Formula ϕ is in conjuntive normal form (CNF) if it is a conjuction of clauses (we also say that ϕ is a CNF formula). We shall often treat a clause as a set of its literals and a CNF formula as a set of its clauses. Thus |ϕ| will denote the number of clauses in ϕ. If two CNF formulas ϕ1 and ϕ2 define the same function, we say that they are equivalent and we denote this fact with ϕ1 ≡ ϕ2. A CNF ψ is called clause minimum if for every CNF ϕ such that ψ ≡ ϕ we have |ψ| ≤ |ϕ|.

Clause C is called an implicate of f if every assignment ⃗x ∈ {0, 1}n satisfying f (i.e. f(⃗x) = 1) also satisfies C (i.e. C(⃗x) = 1). We say that a clause C1 subsumes a clause C2, if every literal from C1 occurs also in C2 (i.e. C1 ⊆ C2). C is a prime implicate of a function f if it is an implicate of f and there is no other implicate C ′ of f subsuming C (i.e. C is a set-minimal implicate of f). We say that CNF formula ϕ is prime if it contains only prime implicates. A CNF formula ϕ is irredundant if there is no sub-CNF ϕ′ ⊂ ϕ which represents the same function as ϕ.

An assignment t which assigns values to only a subset of (possibly to all) variables of a function f on n is called a partial assignment. Formally, partial assignment can be viewed as a mapping t : Y ↦→ {0, 1} where Y is a subset of variables of f. Given a CNF ϕ, ϕ(t) denotes the CNF after applying a partial assignment t.

2.2 Resolution

We say that two clauses have a conflict in variable x if there is a positive occurrence of x in one clause and a negative occurrence in the other. Two clauses C1 = (D1 ∨ x) and C2 = (D2∨x) are resolvable over x if D1 and D2 do not have a conflict in any variable. We write R(C1, C2) = D1 ∨ D2 and this disjunction is called a resolvent of the parent clauses C1 and C2.

2.3 Exclusive Sets of Implicates of a Boolean Function

In this section we follow [Boros et al., 2010]. By I p (f) we shall denote the set of all prime implicates of a function f and by I(f) the resolution closure of I p (f).

Definition 2.1 ([Boros et al., 2010]) Let f be a Boolean function and let X ⊆ I(f) be a set of clauses. We shall say, that X is an exclusive set of clauses of f if for every pair of resolvable clauses C1,C2 ∈ I(f) the following implication holds:

i.e. the resolvent is in X only if both parent clauses are in X.

Theorem 2.2 ([Boros et al., 2010]) Let f be an arbitrary Boolean function, let C1, C2 ⊆ I(f) be two distinct sets of clauses which both represent f, and let X ⊆ I(f) be an exclusive set of clauses. Then C1 ∩ X ≡ C2 ∩ X, i.e. both represent the same function.

Based on this proposition we define an exclusive component of a Boolean function.

Definition 2.3 ([Boros et al., 2010]) Let f be an arbitrary Boolean function, X ⊆ I(f) be an exclusive set of clauses of f, and C ⊆ I(f) be a set of clauses which represents f. The Boolean function fX represented by the set C ∩ X is called the X-component of the function f. We shall simply call a function g an exclusive component of f, if g = fX for some exclusive subset X ⊆ I(f).

Theorem 2.2 guarantees that the X-component fX is well defined for every exclusive set X ⊆ I(f). Theorem 2.2 has the following corollary.

Corollary 2.4 ([Boros et al., 2010]) Let C1, C2 ⊆ I(f) be two distinct sets of clauses such that C1 ≡ C2 ≡ f, i.e. such that both sets represent f, and let X ⊆ I(f) be an exclusive set of clauses. Then (C1 \ X) ∪ (C2 ∩ X) also represents f .

2.4 Autarkies

Autarky is a special type of partial assignment which satisfies each clause in which it substitutes a value for some literal.

Definition 2.5 Let ψ be a CNF on the set V of variables, let Y ⊆ V be a subset of variables, let L = {x | x ∈ Y } ∪ {x | x ∈ Y } be the corresponding set of literals, and let t : Y ↦→ {0, 1} be a partial assignment on ψ. Then t is an autarky on ψ if for every clause C ∈ ψ either C ∩ L = ∅ or C is satisfied by t.

We shall prove two simple lemmas about autarkies which will be needed later in this paper. The first lemma is from [Kullmann, 2000] and the second one is proved in [ ˇCepek et al., 2014].

Lemma 2.6 Let ψ be a CNF on the set V of variables, let Y ⊆ V be a subset of variables, and let t : Y ↦→ {0, 1} be an autarky on ψ. Then t is an autarky on I(f).

Corollary 2.7 Let ψ be a CNF on the set V of variables, let Y ⊆ V be a subset of variables, and let t : Y ↦→ {0, 1} be an autarky on ψ. Let ϕ ⊆ I(f) be an arbitrary representation of f. Then t is an autarky on ϕ.

Let us mention that Corollary 2.7 does not hold without the assumption ϕ ⊆ I(f ). Consider e.g. a CNF ψ = (x ∨ y) ∧ z and a CNF ϕ = (x∨y)∧(z∨y)∧(z∨y). It should be obvious that ψ ≡ ϕ, i.e. both CNFs represent the same function f , but ϕ ̸⊆ I(f). Now if t is an assignment which sets y to 1, t is autarky on ψ. On the other hand t is not autarky on ϕ because (z ∨ y) is not satisfied by t.

Lemma 2.8 Let ψ be a CNF on the set V of variables, let Y ⊆ V be a subset of variables, let L = {x | x ∈ Y } ∪ {x | x ∈ Y } be the corresponding set of literals, and let t : Y ↦→ {0, 1} be an autarky on ψ. Then ψ(t) represents an exclusive component fX of f defined by the exclusive set of clauses

2.5 Matched Formulas

Now we shall define the key concept of this paper. Given an undirected graph G = (V,E), a subset of edges M ⊆ E is a matching in G if the edges in M are pairwise disjoint. A bipartite graph G = (A,B,E) is an undirected graph with disjoint sets of vertices A and B, and the set of edges E satisfying E ⊆ A×B. For a set W of vertices of G, let Γ(W) denote the neighbourhood of W in G, i.e. the set of all vertices adjacent to some element of W. Before giving the definition of matched CNFs let us state the following well-known result on matchings in bipartite graphs:

Theorem 2.9 (Hall's Theorem [Hall, 1935; Lov´asz and Plummer, 1986]) Let G = (A,B,E) be a bipartite graph. A matching M of size |M| = |A| exists if and only if for every subset S of A we have that |S| ≤ |Γ(S)|.

Definition 2.10 Let ϕ = C1 ∧. . .∧Cm be a CNF on n variables X = {x1, . . . , xn}. We shall associate a bipartite graph I(ϕ) = (ϕ,X,E) with ϕ, where the vertices correspond to clauses in ϕ and the variables in X. A clause Ci is connected to a variable xj (i.e. {Ci, xj} ∈ E) if Ci contains xj or xj. A CNF ϕ is matched if I(ϕ) has a matching of size m.

Note that a matching of maximum size in a given graph can be found in polynomial time (see e.g. [Lov´asz and Plummer, 1986]) and thus we can test in polynomial time whether a given CNF is matched. A variable which is matched to some clause in matching M is called matched in M, it is free in M otherwise. Note, that a matched CNF is trivially satisfiable. The name "matched" was given to these formulas in [Franco and Van Gelder, 2003], although they appeared already in [Aharoni and Linial, 1986; Tovey, 1984].

3 Equivalence Testing and Hardness of Clause Minimization of Matched Formulas

Following a definition from [ ˇCepek et al., 2012] a class of CNFs X is called tractable if it satisfies the following four properties.

• Recognition: Given an arbitrary CNF ϕ it is decidable in poly-time with respect to |ϕ| whether ϕ ∈ X .
• Satisfiability: For every CNF ϕ ∈ X it is decidable in poly-time with respect to |ϕ| whether ϕ is satisfiable.
• Partial assignment: Given an arbitrary CNF ϕ ∈ X, if ψ is produced from ϕ by fixing some variables to 0 or 1 and substituting these values into ϕ, then ψ ∈ X .
• Prime representations: Given an arbitrary CNF ϕ ∈ X , if ϕ represents a function f then all prime CNF representations of f belong to X .

It was shown in [ ˇCepek et al., 2012] that given two CNFs from a tractable class, it can be tested in polynomial time, whether these two CNFs are logically equivalent or not. The class of matched CNFs satisfies the first two tractability conditions, but fails to satisfy the remaining two. Constructing a counterexample to the third property is easy. The CNF

is clearly matched, but a partial assignment x ← 0 gives

that is not matched. We defer the counterexample to the fourth property to the next section. In the light of these findings it is an interesting question what is the complexity of equivalence testing for matched CNFs. Surprisingly, despite the fact that satisfiability is trivial for matched CNFs, equivalence testing is co-NP-complete.

MATCHED-EQ

Instance : Two matched CNFs ϕ and ψ

Question : Does ϕ ≡ ψ hold?

Theorem 3.1 MATCHED-EQ is co-NP-complete.

Proof : A nondeterministic polynomial procedure checking that two CNFs are not equivalent guesses an assignment t and checks ϕ(t) ̸= ψ(t). Thus MATCHED-EQ is in co-NP.

To show co-NP-hardness we use reduction from the problem of checking that a given CNF α is unsatisfiable. Let α be an arbitrary CNF on n variables and m clauses, in particular let α = C1 ∧ C2 ∧ . . . ∧ Cm. Let us define a clause D = (a1 ∨ a2 ∨ . . . ∨ am) on m new variables not occurring in α and let us define two CNFs:

Both ϕ and ψ are matched, since each clause C ′ i = (Ci ∨D) can be matched to a variable ai. Because ϕ ≡ α∨D ≡ α∨ψ we have ϕ ≡ ψ iff α ≡ ⊥, i.e. iff α is unsatisfiable.

The fact, that equivalence testing is co-NP-hard, is likely the main reason behind the fact proved in [Gursk´y, 2011]

that clause minimization of matched CNFs is Σp2 -complete. The proof in [Gursk´y, 2011] basically follows the proof of Σp2 -completeness of general Boolean minimization (BM) from [Umans, 2001] and is quite long and complicated. Here we present a much shorter and simpler proof based on a similar idea as the proof for the hardness of equivalence testing.

MATCHED-MIN

Instance : Amatched CNF ϕ and an integer k

Question : ∃ a CNFψ such that ψ ≡ ϕ and |ϕ| ≤ k?

Theorem 3.2 MATCHED-MIN is Σp2 -complete.

Proof : Since MATCHED-MIN is a special case of BM which is known to be Σp2 -complete, MATCHED-MIN is in Σp2 . For the Σp2 -hardness we reduce the Σp2 -complete BM to it.

Let (α, k) be an instance of BM, α = C1 ∧ . . . ∧Cm. Now let us repeat the construction from the proof of Theorem 3.1. Let D = (a1 ∨ . . . ∨ am) be a clause on m new variables not occurring in α, let ϕ = (C1 ∨ D) ∧ . . . ∧ (Cm ∨ D), and let (ϕ, k) be an instance of MATCHED-MIN.

Let (α, k) be a positive instance of BM. Then there exists CNF β = D1∧D2∧. . .∧Dk′ (with k′ ≤ k) that is equivalent to α. Let ψ be a CNF equivalent to β ∨ (a1 ∨ a2 ∨ . . . ∨ am) that is let ψ = D′1 ∧ D′2 ∧ . . . ∧ D′k′ where D′i = Di ∨ a1 ∨ a2 ∨. . .∨am for 1 ≤ i ≤ k′ . Clearly ψ is equivalent to ϕ and has at most k clauses. Therefore (ϕ, k) is a positive instance of MATCHED-MIN.

To see the other direction let (ϕ, k) be a positive instance of MATCHED-MIN and let ψ be a CNF equivalent to ϕ with at most k clauses. Let β be a CNF originating from ψ by a partial assignment that sets all a-variables to zero and sets no other variable. Since ψ is equivalent to ϕ and that is equivalent to α ∨ (a1 ∨ a2 ∨ . . . ∨ am), we have that β is equivalent to α. Clearly |β| ≤ |ψ| ≤ k and since β is equivalent to α we conclude that (α, k) is a positive instance of BM.

4 Prime Representations of Matched Formulas

It is not difficult to see that unlike some well-behaved classes of CNFs (such as e.g. Horn CNFs or quadratic CNFs) for which all prime and irredundant CNFs lie inside the class, this is not the case for matched CNFs. Consider the CNF

which is matched and a logically equivalent CNF

which is not matched despite being prime and irredundant. Thus it is a legitimate question, whether given a (nonprime) matched CNF, there exists at least one logically equivalent prime and irredundant CNF which is also matched. The answer to this question is affirmative, however the proof requires a series of very technical lemmas. Due to the page limit we provide only the final statement here and refer the interested reader to [ ˇCepek et al., 2014].

Theorem 4.1 Let ψ be a matched CNF representing function f. Then there exists a matched CNF ϕ representing f such that ϕ is prime and irredundant.

5 MinimumRepresentations of Matched Formulas

In the previous section we have seen that for a matched CNF there may be some logically equivalent prime and irredundant CNFs which are not matched and some which are matched, the latter set being always non-empty. Here we shall show that a stronger statement holds for CNFs which are not only prime and irredundant but also clause minimum, namely that all such CNFs belong to the latter set.

Theorem5.1 Let ϕbe amatchedCNF representing function f on set of variables V and let ψ be a clause minimum CNF representation of f . Then ψ is a matched CNF.

Proof : Due to Theorem4.1 we may assume that ϕ is prime and irredundant and thus ϕ ⊆ I(f). Let us assume by contradiction that ψ is not matched and that ψX ⊆ ψ is a maximal (under inclusion) sub-CNF violating Hall's condition (such a subset must exist due to Theorem 2.9). Let us denote X the set of variables in the sub-CNF ψX, Y = V \ X the set of remaining variables in ψ, and ψY = ψ \ ψX the remaining clauses in ψ (note that clauses in ψY may contain variables not only from Y but also from X). Now the following holds:

• By the violation of Hall's condition |ψX| > |X| holds.
• By the maximality of ψX there exists a matching M of all clauses in ψY to variables in Y , i.e. ψY is a matched CNF even if we drop all variables in X from its clauses. This follows from the fact that every subset of ψY must satisfy Hall's condition even with respect to the variables in Y , since otherwise any such violating subset could be added to ψX contradicting its maximality.

The existence of matching M implies that ψY can be satisfied using only variables from Y (each clause can be satisfied by its matched variable). So let t : Y ↦→ {0, 1} be some partial assignment satisfying all clauses in ψY (t is not necessarily unique). Clearly, t is an autarky on ψ as it satisfies every clause containing an assigned literal.

It follows from Lemma 2.8 that ψ(t) = ψX represents an exclusive component fX of f defined by the exclusive set X ⊆ I(f), which contains all clauses consisting only of variables from X. Since ϕ also represents f and we assumed ϕ ⊆ I(f), it follows from Corollary 2.7 that t is an autarky also on ϕ. Thus, similarly as for ψ(t) above, we can conclude that ϕ(t) is a sub-CNF of ϕ which represents the exclusive component fX of f, i.e. ψ(t) ≡ ϕ(t). However, ϕ is matched, so every its sub-CNF (and in particular ϕ(t)) is matched, and thus |ϕ(t)| ≤ |X| while |ψ(t)| = |ψX| > |X|. But now, since both ϕ(t) and ψ(t) = ψX represent an exclusive component of f, also CNF ψ′ = (ψ \ ψ(t)) ∪ ϕ(t) represents f by Corollary 2.4. However, we get |ψ′ | < |ψ| contradicting the assumed minimality of ψ.

Acknowledgments

The authors gratefully acknowledge a support by the Czech Science Foundation (grant P202/15-15511S).