Do Hard SAT-Related Reasoning Tasks Become Easier in the Krom Fragment?

1 Introduction

By Schaefer's famous theorem [Schaefer, 1978], we know that the SAT problem becomes tractable under certain syntactic restrictions such as the restriction to Horn formulas (i.e., formulas in CNF where clauses have at most one positive literal) or to Krom formulas (i.e., clauses have at most two literals). Propositional formulas play an important role in reasoning problems in a great variety of areas such as belief change, logic-based abduction, closed-world reasoning, etc. Most of the relevant problems in these areas are intractable. It is therefore a natural question whether restrictions on the formulas involved help to decrease the high complexity. While the restriction to Horn formulas is usually well studied, other restrictions in Schaefer's framework have received much less attention. In this work, we have a closer look at the restriction to Krom formulas and its effect on the complexity of several hard reasoning problems from the AI domain.

One particular source of complexity of such problems is the involvement of some notion of minimality. In closed world reasoning, we add negative literals or more general formulas to a theory only if they are true in every minimal model of the theory in order to circumvent inconsistency. In abduction, we search for a subset of the hypotheses (i.e., an "explanation") that is consistent with the given theory and which - together with the theory - explains (i.e., logically entails) all manifestations. Again, one is usually not contented with any subset of the hypotheses but with a minimal one. However, different notions of minimality might be considered, in

Reinhard Pichler and StefanWoltran

Vienna University of Technology Favoritenstraße 9-11 A-1040 Vienna, Austria

particular, minimality w.r.t. set inclusion or w.r.t. cardinality. In abduction, these two notions are directly applied to explanations [Eiter and Gottlob, 1995]. In belief revision, one is interested in the models of the new belief which have minimal distance from the models of the given belief set. Distance between models is defined here via the symmetric set difference ∆ of the atoms assigned to true in the compared models. Dalal's revision operator [Dalal, 1988] seeks to minimize the cardinality of ∆ while Satoh's operator [Satoh, 1988] defines the minimality of ∆ in terms of set inclusion.

The chosen notion of minimality usually has a significant impact on the complexity of the resulting reasoning tasks. If minimality is defined in terms of cardinality, we often get problems that are complete for some class ∆kP[O(logn)] with k ≥ 2 (which is also referred to as ΘkP, [Wagner, 1988]). For instance, two of the most common reasoning tasks in belief revision (i.e., model checking and implication) are Θ2P-complete for Dalal's revision operator [Eiter and Gottlob, 1992; Liberatore and Schaerf, 2001]. Abduction aiming at cardinality-minimal explanations is Θ3P-complete [Eiter and Gottlob, 1995]. If minimality is defined in terms of set inclusion, completeness results for one of the classes ΣkP or ΠkP for some k ≥ 2 are more common. For instance, belief revision with Satoh's revision operator becomes Σ2P-complete (for model checking) [Liberatore and Schaerf, 2001] respectively Π2P-complete (for implication) [Eiter and Gottlob, 1992]. Similarly, abduction is Σ2P-complete if we test whether some hypothesis is contained in a subsetminimal explanation [Eiter and Gottlob, 1995].

For the above mentioned problems, various ways to decrease the complexity have been studied. Indeed, in almost all of these cases, a restriction of the involved formulas to Horn makes the complexity drop by one level in the polynomial hierarchy. Only belief revision with Dalal's revision operator remains Θ2P-complete in the Horn case, see [Eiter and Gottlob, 1992; Liberatore and Schaerf, 2001; Eiter and Gottlob, 1995]. The restriction to Krom has not been considered yet for these problems. In this paper we show that the picture is very similar to the Horn case. Indeed, for the considered problems in belief revision and abduction, we get for the Krom case exactly the same complexity classifications. Actually, we choose the problem reductions for our hardness proofs in such a way that we thus also strengthen the previous hardness results by showing that they even hold if formulas are restricted to Horn and Krom at the same time.

To get a deeper understanding why belief revision with Dalal's revision operator remains Θ2P-complete in the Krom case, we have a closer look at a related variant of the SAT problem, where also cardinality minimality is involved, namely the CARDMINSAT problem: given a propositional formula ϕ and an atom x, is x true in some cardinalityminimal model of ϕ? It is easy to show that this problem is Θ2P-complete. If ϕ is restricted to Horn, then this problem becomes trivial, since Horn formulas have a unique minimal model which can be efficiently computed. But what happens if we restrict ϕ to Krom? We show that Θ2P-completeness holds also in this case. This hardness result will then also be very convenient for proving our Θ2P-hardness results for the considered problems in belief revision and abduction. Since CARDMINSAT seems to be central in evaluating the complexity of reasoning problems in which a cardinalityminimality is involved we investigate its complexity in a deeper way, in particular by characterizing the tractable cases.

The main results of the paper are as follows:

• SAT variants. In Section 3, we investigate the complexity of the CARDMINSAT problem and the analogously defined CARDMAXSAT problem. Our central result is that these problems remain Θ2P-complete for formulas in Krom form.
• Applications. We investigate several reasoning problems in the areas of belief revision (in Section 4) and abduction (in Section 5). For the restriction to Krom form, we establish the same complexity classifications as for the previously known restriction to Horn form. In fact, we thus also strengthen the previously known hardness results by showing that hardness even holds for the restriction to Horn and Krom.
• Classification of CARDMINSAT inside the Krom fragment. In Section 6 we investigate the complexity of CARDMINSAT within the Krom fragment in order to identify the necessary additional syntactic restrictions towards tractability. To this aim we use the well-known framework by Schaefer and obtain a complete complexity classification of the problem.

2 Preliminaries

Propositional logic. We assume familiarity with the basics of propositional logic [Ben-Ari, 2003]. We only want to fix some notation and conventions here. We say that a formula is in k-CNF (resp. k-DNF) for k ≥ 2 if all its clauses (resp. implicants) have at most k literals. Formulas in 2-CNF are also called Krom. A formula is called Horn (resp. dual Horn) if it is in CNF and in each clause at most one literal is positive (resp. negative). It is convenient to identify truth assignments with the set of variables which are true in an assignment. It is thus possible to consider the cardinality and the subset-relation on the models of a formula. If in addition an order is defined on the variables, we may alternatively identify truth assignments with bit vectors, where we encode true (resp. false) by 1 (resp. 0) and arrange the propositional variables in decreasing order. We thus naturally get a lexicographical order on truth assignments.

Complexity Classes. All complexity results in this paper refer to classes in the Polynomial Hierarchy (PH) [Papadimitriou, 1994]. The building blocks of PH are the classes P and NP of decision problems solvable in deterministic resp. non-deterministic polynomial time. The classes ∆kP, ΣkP, and ΠkP of PH are inductively defined as ∆0P = Σ0P = Π0P = P and ∆k+1P = PΣkP, Σk+1P = NPΣkP, Πk+1P = co-Σk+1P, where we write PC (resp. NPC ) for the class of decision problems that can be decided by a deterministic (resp. non-deterministic) Turing machine in polynomial time using an oracle for the class C. The prototypical ΣkP-complete problem is ∃-QSATk, (i.e., quantified satisfiability with k alternating blocks of quantifiers, starting with ∃), where we have to decide the satisfiability of a formula ϕ = ∃X1∀X2∃X3 . . . QXkψ (with Q = ∃ for odd k and Q = ∀ for even k) with no free propositional variables. W.l.o.g., one may assume here that ψ is in 3-DNF (if Q = ∀), resp. in 3CNF (if Q = ∃). In [Wagner, 1988], several restrictions on the oracle calls in a ∆kP computation have been studied. If on input x with |x| = n at most O(log n) calls to the Σk-1P oracles are allowed, then we get the class PΣk-1P[O(logn)] which is also referred to as ΘkP. A large collection of Θ2Pcomplete problems can be obtained from [Krentel, 1988; Gasarch et al., 1995]. Problems complete for ΘkP with k ≥ 3 can be found in [Krentel, 1992].

3 Θ2P-complete variants of SAT

In this section, we study two natural variants of SAT:

CARDMINSAT Problem

Instance. Propositional formula ϕ and an atom xi.

Question. Is xi true in a cardinality-minimal model of ϕ?

CARDMAXSAT Problem

Instance. Propositional formula ϕ and an atom xi.

Question. Is xi true in a cardinality-maximal model of ϕ?

To analyse the complexity of these problems, we recall the following Θ2P-complete problem from [Krentel, 1988]:

LOGLEXMAXSAT Problem

Instance. Propositional formula ϕ and an order x1 > · · · > xℓ on some of the variables in ϕ with ℓ ≤ log |ϕ|.

Question. Is xℓ true in the lexicographically maximal bit vector (b1, . . . , bℓ) that can be extended to a model of ϕ?

Theorem 1 ([Krentel, 1988]) The LOGLEXMAXSAT problem is Θ2P-complete. The hardness holds even if ϕ is in 3CNF.

From this we get the following Θ2P-completeness result:

Proposition 2 CARDMAXSAT is Θ2P-complete. The hardness holds even if ϕ is in 3-CNF.

Proof. The membership proof proceeds by the classical binary search [Papadimitriou, 1994] for finding the optimum, asking questions like "Does there exist a model of size at least k?". When the maximal size M of all models of ϕ has thus been computed, we check in a final question to an NP-oracle if xi is true in a model of size M.

The Θ2P-hardness of CARDMAXSAT is shown by reduction from LOGLEXMAXSAT. Consider an arbitrary instance of LOGLEXMAXSAT, which is given by a propositional formula ϕ and an order x1 > · · · > xℓ over logarithmically many variables from ϕ. From this we construct an instance of CARDMAXSAT, which will be defined by a propositional formula ψ and a dedicated variable in ψ, namely xℓ. The formula ψ is obtained from ϕ by adding the following subformulas. We simulate the lexicographical order over the variables x1 > · · · > xℓ by adding "copies" of each variable xi, i.e., for every i ∈ {1, . . . , ℓ}, we introduce 2ℓ-i - 1 new variables x(1) i , x(2) i , . . . , x(ri) i with ri = 2ℓ-i - 1. Moreover, we add to ϕ the conjuncts (xi ↔ x(1) i ) ∧ · · · ∧ (xi ↔ x(ri) i ). Hence, setting xi to true in a model of the resulting formula forces us to set all its 2ℓ-i - 1 "copies" to true. Finally, for the remaining variables xℓ+1, . . . , xn in ϕ, we add "copies" x′ℓ+1 , . . . , x′n and further extend ϕ by the conjuncts (xℓ+1 ↔ ¬x′ℓ+1 )∧· · ·∧(xn ↔ ¬x′n ) to make the cardinality of models indistinguishable on these variables.

Since ℓ ≤ log |ϕ|, this transformation of ϕ into ψ is feasible in polynomial time. We claim that our problem reduction is correct, i.e., let ⃗b = (b1, . . . , bℓ) denote the lexicographically maximal vector that can be extended to a model of ϕ. We claim that xℓ is true in a model I of ϕ, s.t. I is an extension of ⃗b iff xℓ is true in a cardinality-maximal model of ψ. In fact, even a slightly stronger result can be shown, namely: if a model of ϕ is an extension of ⃗b, then I can be further extended to a cardinality maximal model J of ψ. Conversely, if J is a cardinality maximal model of ψ, then J is also a model of ϕ and J extends ⃗b. ✷

Our ultimate goal in this section is to show that the Θ2Pcompleteness of CARDMAXSAT and also of CARDMINSAT hold even if restricted to the Krom case. In a first step, we reduce the CARDMAXSAT problem to a variant of the INDEPENDENT SET problem, which we define next. Note that the standard reduction from 3SAT to INDEPENDENT SET [Papadimitriou, 1994] is not sufficient: suppose we are starting off with a propositional formula ϕ with K clauses. Then, if ϕ is satisfiable, every maximum independent set selects precisely K vertices. Hence, additional work is needed to preserve the information on the cardinality of the models of ϕ.

MAXINDEPENDENTSET Problem

Instance. Undirected graph G = (V,E), vertex v ∈ V , and positive integer K.

Question. Is v in a maximum independent set I of G with |I| ≥ K?

Lemma 3 The MAXINDEPENDENTSET problem is Θ2Phard.

Proof. We extend the standard reduction from 3SAT to INDEPENDENT SET [Papadimitriou, 1994] to a reduction from CARDMAXSAT to MAXINDEPENDENTSET. Let (ϕ, x) denote an arbitrary instance of CARDMAXSAT with ϕ = c1 ∧ · · · ∧ cm, s.t. each clause ci is of the form ci = li1 ∨ li2 ∨ li3 where each lij is a literal. Let X = {x1, . . . , xn} denote the set of variables in ϕ. We construct an instance (G, v,K) of MAXINDEPENDENTSET where K := L ∗ m with L "sufficiently large", e.g., L := n + 1; G consists of 3 ∗ L + n vertices V = {l(j) i1 , l(j) i2 , l(j) i3 } | 1 ≤ i ≤ m and 1 ≤ j ≤ L} ∪ {u1, . . . , un}; and v := ui, for x = xi. It remains to specify the edges E of G:

(1) For every i ∈ {1, . . . ,m} and every j ∈ {1, . . . ,L}, E contains edges [l(j) i1 , l(j) i2 ], [l(j) i1 , l(j) i3 ], and [l(j) i2 , l(j) i3 ], i.e., G contains L triangles {l(j) i1 , l(j) i2 , l(j) i3 } with j ∈ {1, . . . , L}.

(2) For every α, β, γ, δ, s.t. lαβ and lγδ are complementary literals, E contains L edges [l(i) αβ , l(j) γδ ] with i, j ∈ {1, . . . , L}.

(3) For every i ∈ {1, . . . , n} and every α, β, if lαβ is of the

form ¬xi, then E contains L edges [l(j)

αβ , ui] (j ∈ {1, . . . , L}).

The intuition of this reduction is as follows: The L∗m triangles {l(j) i1 , l(j) i2 , l(j) i3 } correspond to L copies of the standard reduction from 3SAT to INDEPENDENT SET [Papadimitriou, 1994]. Likewise, the edges between complementary literals are part of this standard reduction. It is easy to verify that for every independent set I with |I| ≥ K, there also exists an independent set I ′ with |I ′ | ≥ |I|, s.t. I ′ chooses from every copy of a triangle the "same" endpoint, i.e., for every i ∈ {1, . . . ,m}, if l(β) iα ∈ I ′ and l(δ) iγ ∈ I ′ , then α = γ.

Since L = n + 1, the desired lower bound K = L ∗ m on the independent set can only be achieved if exactly one vertex is chosen from each triangle. We thus get the usual correspondence between models of ϕ and independent sets of G of size ≥ K. Note that this correspondence leaves some choice for those variables x where the independent set contains no vertex corresponding to the literal ¬x. In such a case, we assume that the variable x is set to true since in CARDMAXSAT, our goal is to maximize the number of variables set to true. Then a vertex ui may be added to an independent set I with |I| ≥ K, only if no vertex l(j) αβ corresponding to a literal lαβ of the form ¬xi has been chosen into the independent set. Hence, ui ∈ I iff xi is to true in the corresponding model of ϕ. ✷

Theorem 4 CARDMAXSAT (resp. CARDMINSAT) remains Θ2P-complete even if we restrict ϕ to Krom and moreover the clauses consist of negative (resp. positive) literals only.

Proof. Membership follows from Proposition 2.

For hardness, we start with the case of CARDMAXSAT. To this end, we first reduce MAXINDEPENDENTSET to the following intermediate problem: Given an undirected graph G = (V,E) and vertex v ∈ V , is v in a maximum independent set I of G? The fact that this intermediate problem reduces to CARDMAXSAT then follows by expressing this problem via a Krom formula with propositional variables V and clauses ¬vi ∨ ¬vj for every edge [vi, vj] in E.

Hence, let us turn to the first reduction and consider an arbitrary instance (G, v,K) of MAXINDEPENDENTSET with G = (V,E) and v ∈ V . We define the corresponding instance (H, v) of the intermediate problem with H = (V ′ , E′ ) where V ′ = V ∪ U with U = {u1, . . . , uK} for fresh vertices ui, and E′ = E ∪ {[ui, vj] | 1 ≤ i ≤ K, vj ∈ V }. The additional edges in E′ make sure that an independent set of H contains either only vertices from V or only vertices from U. Clearly, H contains the independent set U with |U| = K. This shows Θ2P-hardness of CARDMAXSAT.

To show the Θ2P-hardness result for CARDMINSAT, we now can give a reduction from CARDMAXSAT restricted to negative literals. Given, such a CARDMAXSAT instance (ϕ, x) we construct ( ˆ ϕ, x) where ˆ ϕ is given as

The intuition of variables x′ , x′′ is to represent that x is assigned to false. We have the following observations: (1) a cardinality-minimal model of ˆ ϕ either sets x or jointly, x′ and x′′ , to true (for each variable x ∈ var(ϕ)); i.e. it is of the form τ(I) := I ∪ {x′ , x′′ | x ∈ var(ϕ) \ I} for some I ⊆ var(ϕ); (2) for each I ⊆ var(ϕ), it holds that I is a model of ϕ iff τ(I) is a model of ˆ ϕ; (3) for each I, J ⊆ var(ϕ), |I| ≤ |J| iff |τ(I)| ≥ |τ(J)|. It follows that ( ˆ ϕ, x) is a yes-instance of CARDMINSAT iff (ϕ, x) is a yes-instance of CARDMAXSAT. ✷

4 Belief Revision

Belief revision aims at incorporating a new belief, while changing as little as possible of the original beliefs. We assume that a belief set is given by a propositional formula ψ and that the new belief is given by a propositional formula µ. Revising ψ by µ amounts to restricting the set of models of µ to those models which are "closest" to the models of ψ. Several revision operators have been proposed which differ in how they define what "closest" means. Here, we focus on the revision operators due to Dalal [1988] and Satoh [1988].

Dalal's operator measures the distance between the models of ψ and µ in terms of the cardinality of model change, i.e., let M and M ′ be two interpretations and let M∆M ′ denote the symmetric difference between M and M ′ , i.e., M∆M ′ = (M \ M ′ ) ∪ (M ′ \ M). Further, let |∆|min (ψ, µ) denote the minimum number of propositional variables on which the models of ψ and µ differ. We define |∆|min (ψ, µ) := min{|M∆M ′ | : M ∈ mod(ψ),M ′ ∈ mod(µ)}, where mod(·) denotes the models of a formula. Dalal's operator is now given as: mod(ψ ◦D µ) = {M ∈ mod(µ) : ∃M ′ ∈ mod(ψ) s. t. |M∆M ′ | = |∆|min (ψ, µ)}.

Satoh's operator interprets the minimal change in terms of set inclusion. Thus let ∆min (ψ, µ) = min⊆({M∆M ′ : M ∈ mod(ψ), M ′ ∈ mod(µ)}), where the operator min⊆(·) applied to a set S of sets selects those elements s ∈ S, s.t. S contains no proper subset of s. Then we define Satoh's operator as mod(ψ ◦S µ) = {M ∈ mod(µ) : ∃M ′ ∈ mod(ψ) s. t. M∆M ′ ∈ ∆min (ψ, µ)}.

Let ◦r denote a revision operator with r ∈ {D, S}. We analyse two well-studied problems in belief revision.

BR-IMPLICATION Problem

Instance. Propositional formulas ψ and µ, and an atom x.

Question. Does ψ ◦r µ |= x hold?

BR-MODEL CHECKING Problem

Instance. Propositional formulas ψ and µ, and model M of µ. Question. Does M |= ψ ◦r µ hold?

The complexity of these problems has been intensively studied [Eiter and Gottlob, 1992; Liberatore and Schaerf, 2001]. For arbitrary propositional formulas ψ and µ, both problems are Θ2P-complete for Dalal's revision operator. For Satoh's revision operator, BR-MODEL CHECKING (resp. BR-IMPLICATION) is Σ2P-complete (resp. Π2P-complete). Both [Eiter and Gottlob, 1992] and [Liberatore and Schaerf, 2001] have also investigated the complexity of some restricted cases (e.g., when the formulas are restricted to Horn). Below, we pinpoint the complexity of these problems in the Krom case.

Theorem 5 BR-IMPLICATION and BR-MODEL CHECKING are Θ2P-complete for Dalal's revision operator even if the formulas ψ and µ are restricted to Krom and Horn form.

Proof. The membership even holds without any restriction [Eiter and Gottlob, 1992; Liberatore and Schaerf, 2001]. The hardness is shown as follows: Given an instance (ϕ, x0) of CARDMINSAT where X = {x0, x1, . . . , xn} is the set of variables in ϕ. By Theorem 4, this problem is Θ2P-complete even if ϕ is in Krom form with positive literals only. We define the following instances of BR-IMPLICATION and BRMODEL CHECKING:

Let C = {c1, . . . , cm} denote the set of clauses in ϕ. Let X = {x0, . . . , xn} be a set of variables and let y, z be two further variables. We define ψ and µ as:

Then µ has exactly two models M = M1 = {x1, . . . , xn} and M2 = {x1, . . . , xn, x0, y}. Let k denote the size of a minimum model of ϕ. We claim that x0 is contained in a minimum model of ϕ iff M |= ψ ◦D µ iff ψ ◦D µ ̸|= y. The second equivalence is obvious. We prove both directions of the first equivalence separately.

First, suppose that ϕ has a minimum model N with x0 ∈ N. Then the minimum distance of M1 from models of ψ is k, which is witnessed by the model I = X \ N of ψ. It can be easily verified that M2 does not have smaller distance from any model of ψ. At best, M2 also has distance k, namely from any model I2 of ψ of the form I2 = (X \N ′ ) ∪{y}, s.t. N ′ is a minimummodel of ϕ.

Now suppose that every model N of ϕ with x0 ∈ N has size ≥ k+1. Then the distance of M1 from any model I1 of ψ is k+1, since M1∆I1 contains y and at least k elements from {x1, . . . , xn}. On the other hand, the distance of M2 from models of ψ is k witnessed by any model I2 = (X\N ′ )∪{y} of ψ where N ′ is a minimum model of ϕ.

In summary, we have thus shown that M2 |= ψ ◦D µ is guaranteed to hold. But M1 |= ψ ◦D µ holds if and only if there exists a minimummodel N of ϕ with x0 ∈ N. ✷

The above theorem states that, for Dalal's revision operator, the complexity of the BR-IMPLICATION and BRMODEL CHECKING problem does not decrease even if the formulas are restricted to Krom and Horn form. In contrast, we shall show below that for Satoh's revision, the complexity of BR-IMPLICATION and BR-MODEL CHECKING drops one level in the polynomial hierarchy if ψ and µ are Krom. Hence, below, both the membership in case of Krom form and the hardness (which even holds for the restriction to Horn and Krom form) need to be proved.

Theorem 6 BR-IMPLICATION is coNP-complete and BRMODEL CHECKING is NP-complete for Satoh's operator if the formulas ψ and µ are restricted to Krom. Hardness holds even if ψ and µ are further restricted to Krom and Horn.

Proof. For the membership proofs, recall the coNPmembership and NP-membership proof of BRIMPLICATION and BR-MODEL CHECKING for the Horn case in [Eiter and Gottlob, 1992], Theorem 7.2; resp. [Liberatore and Schaerf, 2001], Theorem 20. The key idea there is that, given a model I of ψ and a model M of µ the subset-minimality of I∆M can be tested in polynomial time by reducing this problem to a SAT problem involving the formulas ψ and µ. The same idea holds for Krom form.

The hardness is shown by the following reduction from 3SAT respectively co-3SAT: Let ϕ be an arbitrary Boolean formula in 3-CNF over the variables X = {x1, . . . , xn}, i.e., ϕ = c1 ∧ · · · ∧ cm, s.t. each clause ci is of the form ci = li1 ∨ li2 ∨ li3, where the lij's are literals over X. Let Y = {y1, . . . , yn}, A = {a1, . . . , am}, B = {b1, . . . , bm}, and {d} be sets of fresh, pairwise distinct propositional variables. We define ψ and µ as follows:

where we set l∗ jk = xα if ljk = xα for some α ∈ {1, . . . , n} and l∗ jk = yα if ljk = ¬xα. Finally, we define M = X ∪ Y ∪ A. We claim that ϕ is satisfiable iff M |= ψ ◦S µ iff ψ ◦S µ ̸|= d.

Clearly, every model of µ must set the variables in X ∪ Y ∪ A to true. The truth value of the variables in B may be chosen arbitrarily. However, as soon as at least one bj ∈ B is set to true, we must set d to true due to the last conjunct in µ. Hence, M is the only model of µ where d is set to false. From this, the second equivalence above follows. Below we sketch the proof of the first equivalence.

First, suppose that ϕ is satisfiable and let G be a model of ϕ. We set I := {xi | xi ∈ G}∪{yi | xi ̸∈ G}. Clearly, I is a model of ψ. We claim that I is a witness for M |= ψ◦S µ, i.e., I∆M is minimal. To prove this claim, let J be a model of ψ and N a model of µ, s.t. J∆N ⊆ I∆M. It suffices to show that then J∆N = I∆M holds. To this end, we compare I and J first on X ∪ Y then on A and finally on B ∪ {d}: By the first group of conjuncts in ψ, we may conclude from J∆N ⊆ I∆M that I and J coincide on X∪Y . In particular, both I and J are models of ϕ. But then they also coincide on A since the second group of conjuncts in ψ enforces I(aj) = J(aj) = false for every j. Note that (I∆M)∩(B∪{d}) = ∅. Hence, no matter how we choose J and N on B ∪ {d}, we have I∆M ⊆ J∆N.

Now suppose that ϕ is unsatisfiable. Let I be a model of ψ. To prove M ̸|= ψ ◦S µ, we show that I∆M cannot be minimal. By the unsatisfiability of ϕ, we know that I (restricted to X) is not a model of ϕ. Hence, there exists at least one clause cj which is false in I. The proof goes by constructing J,N with J∆N ⊂ I∆M. The crucial observation is that the symmetric difference I∆M can be decreased by setting J(aj) = J(bj) = N(bj) = true and N(d) = true. ✷

5 Propositional Abduction

Abduction is used to produce explanations for some observed manifestations. Therefore one of its primary fields of application is diagnosis. A propositional abduction problem (PAP) P consists of a tuple 〈V,H,M, T〉, where V is a finite set of variables, H ⊆ V is the set of hypotheses, M ⊆ V is the set of manifestations, and T is a consistent theory in the form of a propositional formula. A set S ⊆ H is a solution (also called explanation) to P if T ∪ S is consistent and T ∪ S |= M holds. A system diagnosis problem can be represented by a PAP P = 〈V,H,M, T〉 as follows. The theory T is the system description. The hypotheses H ⊆ V describe the possibly faulty system components. The manifestations M ⊆ V are the observed symptoms, describing the malfunction of the system. The solutions S of P are the possible explanations of the malfunction.

Often, one is not interested in any solution of a given PAP P but only in minimal solutions, where minimality is defined w.r.t. some preorder ⪯ on the powerset 2H . Two natural preorders are set-inclusion ⊆ and smaller cardinality denoted as ≤. Note that allowing any solution corresponds to choosing "=" as the preorder. In [Creignou and Zanuttini, 2006] a trichotomy (of Σ2P-completeness, NP-completeness, and tractability) has been proved for the SOLVABILITY problem of propositional abduction, i.e., deciding if a PAP P has at least one solution (the preorder "=" has thus been considered). Nordh and Zanuttini [2008] have identified many further restrictions which make the SOLVABILITY problem tractable. All of the above mentioned preorders have been systematically investigated in [Eiter and Gottlob, 1995]. A study of the counting complexity of abduction with these preorders has been carried out by Hermann and Pichler [2010]. Of course, if a PAP has any solution than it also has a ⪯- minimal solution. Hence, the preorder is only of interest for problems like the following one:

⪯-RELEVANCE Problem

Instance. PAP P = 〈V, H, M, T 〉 and hypothesis h ∈ H. Question. Is h relevant, i.e., does P have a ⪯-minimal solu-

tion S with h ∈ S?

Known results [Eiter and Gottlob, 1995] are as follows: The ⪯-RELEVANCE problem is Σ2P-complete for preorders = and ⊆ and Θ3P-complete for preorder ≤. Moreover, the complexity drops by one level in the polynomial hierarchy if the theory is restricted to Horn. In [Creignou and Zanuttini, 2006], the Krom case has been considered for the preorder

=. Below we show that also for the preorders ⊆ and ≤, the complexity in the Krom case matches the Horn case.

Theorem 7 Suppose that we only consider PAPs P = 〈V,H,M, T〉 where the theory T is Krom. Then ⪯- RELEVANCE is NP-complete for preorder ⊆ and Θ2Pcomplete for preorder ≤. The hardness results hold even if the theory is restricted simultaneously to Horn and Krom.

Proof. The membership proofs are analogous to the corresponding ones in [Eiter and Gottlob, 1995] for the general case. The decrease of complexity is due to the tractability of satisfiability testing in the Krom case. Hardness is shown by the following problem reductions:

(1) NP-hardness for preorder ⊆. Consider an arbitrary instance ϕ of 3SAT. Let ϕ be a formula with variables in X = {x1, . . . , xn} of the form ϕ = c1 ∧ · · · ∧ cm with ci = li1 ∨ li2 ∨ li3. We define sets X′ = {x′1 , . . . , x′n}, G = {g1, . . . , gm}, Q = {q1, . . . , qn}, and {r, t} of fresh, pairwise distinct variables, and P = 〈V, H, M, T 〉 with

where l∗ ij is defined as l∗ ij = xα if lij = xα for some α ∈ {1, . . . , n} and l∗ ij = x′α i lij = ¬xα.

The clauses in the first line of T make sure that, for every i ∈ {1, . . . , n}, every solution of P contains exactly one of the variables xi and x′i . For any set I ⊆ X, let I ′ := {x′i | xi ∈ I}. Then the clauses in the second line of T guarantee that all solutions of P have the form I ∪ (X′ \ I ′ ) ∪ {r} for some I ⊆ X. Hence, every solution is ⊆-minimal. Moreover, we have that I is a model of ϕ iff I ∪ (X′ \ I ′ ) ∪ {r} is a solution of P. Hence, ϕ is satisfiable iff r is contained in a ⊆-minimal solution of P.

(2) Θ2P-hardness for preorder ≤. We proceed by reduction from CARDMINSAT. Consider an arbitrary instance (ϕ, xi) of CARDMINSAT with ϕ. By Theorem 4, we may assume that ϕ is in positive Krom form. Let ϕ = (p1 ∨ q1) ∧ · · · ∧ (pm ∨ qm) over variables X = {x1, . . . , xn} and let G = {g1, . . . , gm} be a set of fresh, pairwise distinct variables. We define the PAP P = 〈V, H, M, T 〉 as follows:

Obviously, the models of ϕ coincide with the solutions of P. Hence, xi is in a minimummodel of ϕ iff xi is in a minimum solution of P. ✷

6 Complete Classification of CARDMINSAT

Since neither the full Krom fragment nor even the Krom and (dual) Horn fragment makes the problems investigated tractable (especially the ones that are Θ2P-complete) it is worth making a step further and studying how much we have to restrict the syntactic form of the Krom formulas to decrease the complexity. A key for such tractability results is to go through a more fine-grained complexity study of CARDMINSAT. To this aim we propose to investigate this problem within Schaefer's framework that we introduce next.

A logical relation of arity k is a relation R ⊆ {0, 1}k . We will refer below to the following binary relation, Or = {(0, 1), (1, 0), (1, 1)}. A constraint (or constraint application) is a formula R(x1, . . . , xk), where R is a logical relation of arity k and x1, . . . , xk are (not necessarily distinct) variables. An assignment I of truth values to the variables satisfies the constraint if (I(x1), . . . , I(xk)) ∈ R. A constraint language Γ is a finite set of logical relations. A Γ-formula, ϕ, is a conjunction of constraint applications using only logical relations from Γ, and hence is a quantifier-free first-order formula. For single-element constraint languages {R}, we often omit parenthesis and speak about R-formulas instead of {R}-formulas. With var(ϕ) we denote the set of variables appearing in ϕ. A Γ-formula ϕ is satisfied by an assignment I if I satisfies all the constraints in ϕ. Assuming a canonical order on the variables, we can regard assignments as tuples in the obvious way, and say that a quantifier-free first-order formula defines or implements the logical relation of its solutions. For instance the binary clause (x1 ∨ x2) defines the relation Or. We say that a Boolean relation R is Horn (resp. Krom) if R can be defined by a CNF formula which is Horn (resp. by a 2-CNF formula). A relation is width-2 affine if it is definable by a conjunction of equalities and disequalities between pairs of variables. Finally, a constraint language Γ is Horn (resp. Krom, width-2 affine) if every relation in Γ is Horn (resp. Krom, width-2 affine).

We study here the problem CARDMINSAT(Γ) where one is given a Γ-formula ϕ and atom x. At first sight this problem can look very similar to the optimisation problem MINONES(Γ) studied by Khanna et al., in which given a Γformula the question is to find a minimal cardinality model. However, the complexity classification obtained in [Khanna et al., 2001] shows NP-hardness and as a consequence is of no help here (where Θ2P-hardness is expected).

Observe that Theorem 4 can be reformulated as: CARDMINSAT(Or) is Θ2P-complete. We obtain the following complete classification result.

Theorem 8 Let Γ be a Krom constraint language. If Γ is width-2 affine or Horn, then CARDMINSAT(Γ) is decidable in polynomial time. Otherwise it is Θ2P-complete.

Proof. Let us first deal with the polynomial cases. Let ϕ be a Γ-formula. Suppose first that Γ is Horn. In this case ϕ can be written as a Horn formula. The unique minimal model of ϕ can be found in polynomial time by unit propagation.

Suppose now that Γ is width-2 affine. Without loss of generality we can suppose that ϕ does not contain unitary clauses. Then each clause of ϕ expresses either the equality or the disequality between two variables. Using the transitivity of the equality relation and the fact that in the Boolean case a ̸= b ̸= c implies a = c, we can identify equivalence classes of variables such that each two classes are either independent or they must have contrary truth values. We call a pair (A, B) of classes with contrary truth values cluster, B may be empty. It follows easily that any two clusters are independent and thus to obtain a model of ϕ, we choose for each cluster (A,B) either A = 1,B = 0 or A = 0,B = 1. We suppose in the following that ϕ is satisfiable (otherwise, we will detect a contradiction while constructing the clusters). The weight contribution of each cluster to a model is either |A| or |B|. It is then enough to consider the cluster (A,B) that contains the atom xi. If xi ∈ A and |A| ≤ |B|, then xi belongs to a cardinality-minimal model of ϕ, else it does not.

Hardness results rely on the application of tools from universal algebra (see, e.g. [Geiger, 1968; Jeavons, 1998; Schnoor and Schnoor, 2008; Nordh and Zanuttini, 2009]). Due to space limitations we only give a sketch of proof and the main ingredients. Let ϕ be a formula and x ∈ var(ϕ), then x is said to be frozen in ϕ if it is assigned the same truth value in all its models. Further, we say that Γ freezingly implements a given relation R if there is a Γ-formula ϕ such that R(x1, . . . xk) ≡ ∃Xϕ, where ϕ uses variables from X ∪ {x1, . . . xk} only, and all variables in X are frozen in ϕ. Observe that in this case we have CARDMINSAT(R) ≤ CARDMINSAT(Γ). Indeed, the implementation gives a procedure to transform any R-formula into a satisfiability equivalent Γ-formula with existentially quantified variables. The fact that the implementation "freezes" the existentially quantified variables makes it possible to remove the quantifiers, while preserving the cardinality-minimal solutions. Therefore, in order to prove that CARDMINSAT(Γ) is Θ2P-hard our main strategy is to exhibit a relation R which can be freezingly implemented by Γ such that CARDMINSAT(R) is Θ2P-hard. Roughly speaking the set of all relations that can be (freezingly) implemented by Γ ∪ {=} forms a (frozen) co-clone. Universal algebra plays there an important role in providing a one-to-one correspondence between the lattice of (partial) co-clones and the well-known Post's lattice of Boolean (partial) functions (see e.g. [Jeavons, 1998; Schnoor and Schnoor, 2008; Nordh and Zanuttini, 2009] for details). Based on the results in [B¨ohler et al., 2005; Nordh and Zanuttini, 2009] one can prove that if Γ is Krom but neither Horn nor 2-affine, then Γ can freezingly implement either the relation Or, or the relation Rp 4 defined by (x1∨x2)∧(x1 ̸= x3)∧(x2 ̸= x4), or the relation S defined by (x2 ∨x3)∧(x1 → x2)∧(x1 → x3)∧(x4). We have seen that CARDMINSAT(Or) is Θ2P-complete. To conclude the proof it is therefore sufficient to prove that CARDMINSAT(Rp 4 ) and CARDMINSAT(S) are Θ2P-hard. These hardness results are obtained by a reduction from CARDMINSAT(Or). Let ϕ = ∧(i,j)∈E Or(xi, xj) be an Or-formula with var(ϕ) = {x1, . . . , xn} and E ⊆ {1, . . . , n}2 .

To prove that CARDMINSAT(Or) ≤ CARDMINSAT(Rp 4 )

we consider the formula ϕ′ built over the set of variables {x1, . . . , xn, x′1 , . . . , x′n , x′′ 1 , . . . , x′′n} and defined by ϕ′ = ∧(i,j)∈E Rp 4 (xi, xj , x′i , x′j ) ∧ Rp 4 (x′′ i , x′′ j , x′i , x′j ). Observe that in every model of ϕ′ , for all i we have xi = x′′ i and xi ̸= x′i . Therefore, it is easily seen that there is a one-to-one correspondence between the set of models of ϕ and the set of models of ϕ′ , preserving the truth values of {x1, . . . , xn} and transforming every model of weight k of ϕ into a model of weight n + k of ϕ′ . Therefore a given atom xi belongs to a cardinality-minimal model of ϕ if and only if it belongs to a cardinality-minimal model of ϕ′ .

To prove that CARDMINSAT(Or) ≤ CARDMINSAT(S) we introduce two fresh variables f and t and consider the Sformula defined by ϕ′ = ∧(i,j)∈E S(f, xi, xj, t). It easy to verify that every cardinality-minimal model of ϕ′ sets f to false and t to true, and thus that a given atom xi belongs to a cardinality-minimal model of ϕ if and only if it belongs to a cardinality-minimal model of ϕ′ . ✷

7 Conclusion

In this work we have investigated how the restriction of propositional formulas to Krom affects the complexity of reasoning problems in the AI domain. Our results on belief revision and abduction are summarized in Table 1, where the complexity classifications for Krom and the combined Horn∩Krom case refer to new results we have provided in the paper. Having shown that the complexity of problems involving cardinality minimality, like Dalal's revision operator or ≤-RELEVANCE in abduction, is often robust to such a restriction (even for formulas being Horn and Krom at the same time), suggests that further classes within the Krom fragment should be considered to identify the exact tractability/intractability frontier.

The problem CARDMINSAT seems to be the key for such investigations, thus we initiated a deeper study by giving a complete classification of that problem restricted to Krom within Schaefer's framework. As a next step, we want to study the Krom form (and the yet more restricted fragments thereof) in the context of further hard reasoning problems and analyse which of these fragments suffice to yield tractability.

Acknowledgments

This research has been supported by the Austrian Science Fund (FWF) through the projects P25518-N23 and P25521N23, by the OeAD project FR 12/2013 and by the Campus France Amadeus project 29144UC.