A Fine-Grained Complexity View on Propositional Abduction - Algorithms and Lower Bounds

1 Introduction

The Boolean satisfiability problem is a well-known NPcomplete problem. Due to the rapid advance of SAT solvers, many combinatorial problems are today solved by reducing to SAT, which can then be solved with off-the-shelf solvers. SAT fundamentally encodes a form of monotonic reasoning in the sense that conclusions remain valid regardless if new information is added. However, the real world is nonmonotonic, meaning that one should be able to retract a statement if new data is added which violates the previous conclusion. One of the best known examples of non-monotonic reasoning is abductive reasoning where we are interested in finding an explanation, vis-`a-vis a hypothesis, of some observed manifestation. Abduction has many practical applications, e.g., scientific discovery [Inoue et al., 2009], network security [Alberti et al., 2005], computational biology [Ray et al., 2006], medical diagnosis [Obeid et al., 2019], knowledge base updates [Sakama and Inoue, 2003], and explainability issues in machine learning and decision support systems [Ignatiev et al., 2019; Ignatiev, 2020; Brarda et al., 2021; Racharak and Tojo, 2021]. This may be especially poignant in forthcoming decades due to the continued emergence of AI

in new and surprising applications, which need to be made GDPR compliant [Sovrano et al., 2020] and explainable. The incitement for solving abduction fast, even when it is classically intractable, thus seems highly practically motivated.

Can non-monotonic reasoning be performed as efficiently as monotonic reasoning, or are there fundamental differences between the two? The classical complexity of abduction (and many other forms of non-monotonic reasoning) is wellknown [Eiter and Gottlob, 1995; Thomas and Vollmer, 2010] and suggests a difference: SAT is NP-complete, while most forms of non-monotonic reasoning, including propositional abduction, are generally ΣP2 -complete. However, modern complexity theory typically tells a different story, where classical hardness results do not imply that the problems are hopelessly intractable, but rather that different algorithmic schemes should be applied. For SAT, there is a healthy amount of theoretical research complementing the advances of SAT solvers, and k-SAT for every k can be solved substantially faster than 2n (where n is the number of variables) via the resolution-based PPSZ algorithm [Paturi et al., 2005]. There is a complementary theory of lower bounds where the central conjecture is that 3-SAT is not solvable in 2o(n) time (exponential-time hypothesis (ETH) [Impagliazzo and Paturi, 2001]) and the strong exponential-time hypothesis (SETH) which implies that SAT with unrestricted clause length (CNFSAT) cannot be solved in cn time for any c < 2.

In contrast, the precise exponential time complexity of abduction is currently a blind spot, and no improved algorithms are known for the intractable cases. In this paper we thus issue a systematic attack on the complexity of abduction with a particular focus on the natural complexity parameter n, the number of variables in the knowledge base, sometimes supplemented by |H| or |M|, the number elements in the hypothesis H or manifestation M. To obtain general results we primarily consider the setup where we are given a set of relations Γ (a constraint language) where the knowledge base of an instance is provided by a Γ-formula. We write ABD(Γ) for this problem and additionally also consider the variant where an explanation only consists of positive literals (P-ABD(Γ)) since these two variants exhibit interesting differences. The classical complexity of abduction is either in P, NP-complete, coNP-complete, or ΣP2 -complete [Nordh and Zanuttini, 2008], and for which intractable Γ is it possible to beat exhaustive search? According to Cygan et al., tools to precisely analyze the exponential time complexity of NPcomplete problems are in its infancy [2016]. For problems at higher levels of the polynomial hierarchy the situation is even more dire. Are algorithmic approaches for problems in NP still usable? Are the tools to obtain lower bounds still usable? Why are no sharp upper bounds known for problems in nonmonotonic reasoning, and are these problems fundamentally different from e.g. satisfiability problems?

We successfully answer many of these questions with novel algorithmic contributions. First, in Section 3 we show why enumerating all possible subsets of the hypothesis gives a bound 2n for ABD and the (surprisingly bad) 3n bound for P-ABD. Hence, any notion of improvement should be measured against 2n for ABD and 3n for P-ABD. Generally improving the factor 2|H| (which may equal 2n ) seems difficult but we do manage this for languages Γ where all possible models of the knowledge base can be enumerated in cn time, for some c ≤ 2, which we call sparsely enumerable languages. We succeed with this for both ABD(Γ) (Section 3.1) and P-ABD(Γ) (Section 3.2), and while the algorithms for the two different cases share ideas, the details differ in intricate ways. It should be remarked that both algorithms solve the substantially more general problem of enumerating all (maximal) explanations which may open up further, e.g., probabilistic, applications for abduction. The enumeration algorithms in addition to exponential time also need exponential memory, but we manage to improve the naive 3n bound for P-ABD(Γ) to 2n with only polynomial memory. The sparsely enumerable property is strong: it fails even for 2-SAT and it is a priori not clear if it is ever true for intractable languages. Despite this, we manage to (in Section 3.3) describe three properties implying sparse enumerability. This captures relations definable by equations x1 +. . .+xk = q (mod p) (EQUATIONSk ). The problem(s) (P-)ABD(EQUATIONS) is ΣP2 -complete and is, to the best of our knowledge, the first example of beating exhaustive search for a ΣP2 -complete problem (under n). This yields improved algorithms for ΣP2 -complete P-ABD(XSAT) (exact satisfiability) and NP-complete P-ABD(AFF(≤k) ) (arity bounded equations over GF(2)).

In Section 3.4 we consider more restricted types of abduction problems with a particular focus on (P-)ABD(k-CNF+) where k-CNF+ contains all positive clauses of arity k. Here, the problems are only NP-complete, in which case circumventing the 2|H| barrier appears easier. For these, and similar, problems, we construct an improved algorithm based on a novel reduction to a problem SIMPLESATp which can be solved by branching. For coNP, only P-ABD(Γ) becomes relevant, and we (in Section 3.5) prove a simple but general improvement whenever a finite Γ is invariant under a constant Boolean operation.

In Section 4, we prove lower bounds under (S)ETH for missing intractable cases. Let IMP = {{(0, 0), (0, 1), (1, 1)}}. Under the ETH, we first prove that ABD(2-CNF+) and ABD(2-CNF- ∪ IMP) cannot be solved in time ( |H| |M| )o(|M|) under ETH, which asymptotically matches exhaustive search. For classical cases like k-CNF (k ≥ 4) and NAE-k-SAT (k ≥ 5) we establish sharp lower bounds of the form 2n for ABD and 1.4142n for P-ABD under the SETH. For (P-)ABD(CNF- ∪ IMP), we rule out improvements to 1.2599n , 1.4142|H| , 2|M| , or ( |H| |M| )|M| under SETH. This transfers to Horn for (P-)ABD and to DualHorn for ABD. For ABD(2-CNF), we prove that sharp lower bounds under the SETH are unlikely unless NP ⊆ P/Poly, leaving its precise fine-grained complexity as an interesting open question.

The results are summarized in Table 1 and Table 2 where (P), respectively (M), indicates that the result only holds for P-ABD, respectively ABD. Thus, put together, we obtain a rather precise picture of the fine-grained complexity of ABD(Γ) and P-ABD(Γ) for almost all classical intractable languages Γ. Notably, we have proven that even ΣP2 -complete problems can admit improved algorithms with respect to n, and that the barrier of exhaustively enumerating all possible explanations can be broken.

Proofs of statements marked with (⋆) can be found in the technical report [Lagerkvist et al., 2025].

2 Preliminaries

We begin by introducing basic notation and terminology.

Propositional logic. We assume familiarity with propositional logic, clauses, and formulas in conjunctive/disjunctive form (CNF/DNF). We denote Var(φ) the variables of a formula φ and for a set of formulas F , Var(F ) = ⋃φ∈F Var(φ). We identify finite F with the conjunction of all formulas from F, that is ∧φ∈F φ. A model of a formula φ is an assignment σ : Var(φ) ↦→ {0, 1} that satisfies φ. For two formulas ψ, φ we write ψ |= φ if every model of ψ also satisfies φ. For a set of variables V , Lits(V ) the set of all literals formed upon V , that is, Lits(V ) = V ∪ {¬x | x ∈ V }.

Boolean constraint languages. A logical relation of arity k ∈ N is a relation R ⊆ {0, 1}k , and ar(R) = k denotes the arity. An (R-)constraint C is a formula C = R(x1, . . . , xk), where R is a k-ary logical relation, and x1, . . . , xk are (not necessarily distinct) variables. An assignment σ satisfies C, if (σ(x1), . . . , σ(xk)) ∈ R. A (Boolean) constraint language Γ is a (possibly infinite) set of logical relations, and a Γ-formula is a conjunction of constraints over elements from Γ. A Γ-formula ϕ is satisfied by an assignment σ, if σ simultaneously satisfies all constraints in it, in which case σ is also called a model of ϕ. We define the two constant unary Boolean relations as ⊥ = {(0)} and ⊤ = {(1)}, and the two constant 0-ary relations as f = ∅ and t = {∅}. We say that a k-ary relation R is represented by a propositional CNF-formula ϕ if ϕ is a formula over k distinct variables x1, . . . , xk and ϕ ≡ R(x1, . . . , xk). Note such a CNFrepresentation exists for any logical relation R ⊆ {0, 1}k . We write CNF for the relations corresponding to all possible clauses and Horn/DualHorn for the set relations corresponding to Horn/DualHorn clauses. Additionally, k-CNF is the subset of CNF of arity k, IMP = {R}, where R(x, y) = {0, 1}2 - {(1, 0)}. The notation (k-)CNF+ (resp. (k-)CNF) denotes the version where each clause is positive (resp. negative). We use AFF to denote the set of relations representable by systems of Boolean equations modulo 2, i.e., x1+. . .+xk ≡ q (mod 2) for q ∈ {0, 1}. As representation of each relation in a constraint language we use the defining CNF-formula unless stated otherwise.

The satisfiability problem for Γ-formulas, also known as Boolean constraint satisfaction problem, is denoted SAT(Γ). It asks, given a Γ-formula ϕ, whether ϕ admits a model.

Propositional Abduction. An instance of the abduction problem over a constraint language Γ is given by (KB,H,M), where KB is a Γ-formula, and H and M sets of variables, referred to as hypothesis and manifestation. We let V = Var(KB) ∪ Var(H) ∪ Var(M) be the set of variables and write n = |V | for its cardinality. The symmetric abduction problem, denoted ABD(Γ), asks whether there exists an E ⊆ Lits(H) such that 1) KB∧E is satisfiable, and 2) KB∧E |=M. If such an E exists, it is called an explanation for M. If an explanation E satisfies Var(E) = H it is called a full explanation, if it satisfies E ⊆ H, it is called a positive explanation. If there exists an explanation E, it can always be extended to a full explanation (by extending E according to the satisfying assignment underlying condition 1). However, the existence of an explanation does not imply the existence of a positive explanation. The positive abduction problem, denoted P-ABD(Γ), asks whether there exists a positive explanation. We write (P-)ABD(Γ) if the specific abduction type is not important.

Example 1. Consider the following example.

E1 = {A, ¬D, ¬E} is a full explanation, and E2 = {A, D} is a positive explanation.

We note at this point that the classical complexity of ABD(Γ) and P-ABD(Γ) is fully determined for all Γ, due to Nordh and Zanuttini [2008]. An illustration of these classifications is found in the technical report [Lagerkvist et al., 2025].

Algebra. We denote by ¯x the Boolean negation operation, that is, f(x) = ¬x. An n-ary projection is an operation f of the form f(x1, . . . , xn) = xi for some fixed 1 ≤ i ≤ n. An operation f : {0, 1}k → {0, 1} is constant if for all x ∈ {0, 1}k it holds f(x) = c, for a c ∈ {0, 1}. For a k-ary operation f : {0, 1}k → {0, 1} and X ⊆ {0, 1}k we write f|X for the function obtained by restricting the domain of f to X. An operation f is a polymorphism of a relation R if for every t1, . . . , tk ∈ R it holds that f(t1, . . . , tk) ∈ R, where f is applied coordinate-wise. In this case R is called closed or invariant, under f, ard Inv(F) denotes the set of all relations invariant under every function in F. Dually, for a set of relations Γ, Pol(Γ) denotes the set of all polymorphisms of Γ. Sets of the form Pol(Γ) are known as clones, and sets of the form Inv(F) are known as co-clones. A clone is a set of functions closed under 1) functional composition, and 2) projections (selecting an arbitrary but fixed coordinate). For a set B of (Boolean) functions, [B] denotes the corresponding clone, and B is called its base. There is an inverse relationship between Pol(Γ) and Inv(F) but we defer the details to the technical report.

Complexity theory. We assume familiarity with basic notions in classical complexity theory (cf. [Sipser, 1997]) and use complexity classes P, NP, coNP, NP NP = ΣP2 . In this paper we work in the setting of parameterized complexity where the complexity parameter is the number of variables n, in either an abduction or SAT instance, or the number of vertices in a graph problem. For a variable problem A we let I(A) be the set of instances and Var(I) the set of variables. If clear from the context we usually write n rather than | Var(I)|.We define the following two types of reductions [Jonsson et al., 2017] (note that ordinary polynomial-time reductions do not necessarily preserve the number of variables).

Definition 2. Be A,B two variable problems. A function f : I(A) → I(B) is a many-one linear variable reduction (LV-reduction) with parameter C ≥ 0 if I is a yes-instance of A iff f(I) is a yes-instance of B, |Var(f(I))| = C · | Var(I)|+O(1), and f can be computed in polynomial time.

If in an LV-reduction the parameter C is 1, we speak of a CV-reduction, and we take us the liberty to view a reduction which actually shrinks the number of variables (|Var(f(I))| ≤ |Var(I)| + O(1)) as a CV-reduction, too. We use A ≤CV B, respectively A ≤LV B as shorthands, and sometimes write A =CV B if A ≤CV B and B ≤CV A. For algorithms' (exponential) running time and space usage we adopt the O∗ notation which suppresses polynomial factors. A CV-reduction transfers exact exponential running time: if A≤CV B, and B can be solved in time O∗ (cn ), then also A can be solved in time O∗ (cn ) (where n denotes the complexity parameter). LV-reductions, on the other hand, preserve subexponential complexity, i.e., if B can be solved in O∗ (cn ) time for every c > 1 and A ≤LV B then A is solvable in O∗ (cn ) time for every c > 1, too. For additional details we refer the reader to [Jonsson et al., 2021b].

3 Upper Bounds via SAT Based Approaches

We begin by investigating the possibility of solving ABD(Γ) and P-ABD(Γ) faster, conditioned by a reasonably efficient algorithm for SAT(Γ). This assumption is necessary to beat exhaustive search since SAT(Γ) ≤CV (P-)ABD(Γ), which implies that if SAT(Γ) is not solvable in O(cn ) time for any c < 2 then (P-)ABD(Γ) is not solvable in O(cn ) time for any c < 2, either.

For a constraint language Γ we let Γ+ = Γ ∪ {⊥, ⊤}, i.e., Γ expanded with the two constant Boolean relations. Trivially, we have SAT(Γ) ≤CV SAT(Γ+), and we observe that if Pol(Γ) does not contain a constant operation then we additionally have SAT(Γ+)≤CV SAT(Γ) [Jonsson et al., 2021a]. We obtain the following baseline bound to beat.

Theorem 3. (⋆) Let Γ be a constraint language such that SAT(Γ+) is solvable in f(n) time for some computable function f : N→N. Then

1. ABD(Γ) is solvable in 2|H| ·f(n-|H|)·(|M|+1) time,

2. P-ABD(Γ) is solvable in ΣE⊆Hf(n- |E|) · (|M| +1) time.

Since every SAT(Γ+) problem is solvable in O∗ (cn ) time for some c ≤ 2 we get an overall bound of 2|H| · O∗ (cn-|H| ) ∈ O∗ (2n ) for ABD(Γ), and ΣE⊆HO∗ (cn-|E| ) = O∗ (cn-|H| · (c + 1)|H| ) ∈ O∗ ((c + 1)n ) ∈ O∗ (3n ) for P-ABD(Γ).

The question is now when these baseline bounds can be beaten. As a general method we (for both ABD and P-ABD) consider the assumption that all models of the knowledge base can be enumerated sufficiently fast.

Definition 4. The set of models of a SAT(Γ) instance φ is denoted Mod(φ). If there exists c < 2 such that |Mod(φ)| ≤ cn then SAT(Γ) is said to be sparse.

We also need the corresponding computational property where we require all models to be enumerable fast.

Definition 5. Let Γ be a constraint language. If Mod(φ), for every SAT(Γ) instance φ, can be enumerated in O∗ (cn ) time for some c < 2 then we say that SAT(Γ) is sparsely enumerable.

3.1 Faster Algorithms for ABD

We handle ABD(Γ) first since the analysis is simpler than for P-ABD(Γ) (in Section 3.2). Trading polynomial for exponential space we consider a faster algorithm for ABD(Γ) under the condition that SAT(Γ) is sparsely enumerable.

We first state a technical lemma, facilitating the presentation of the algorithms and reductions throughout the following sections.

Lemma 6. (⋆) When solving an abduction instance (KB,H,M), we can W.L.O.G. assume that M,H ⊆ Var(KB), via a polynomial time preprocessing. This constitutes even a CV-reduction of the problem to itself.

Now the basic idea to solve ABD(Γ) is to define an equivalence relation ≡H over Mod(KB) by letting f ≡H g if and only if f|H = g|H (where H is the hypothesis set). We then construct the equivalence classes of ≡H and discard a class when it fails to explain M. An explanation exists if there is a non-empty class where every member satisfies M. Initially, this requires exponential space, O∗ (2n ). However, by only storing information on whether a potential explanation E has an extension that fails to satisfy M, space usage is reduced to O∗ (2|H| ). The space usage is further limited by the enumerating algorithm's runtime, O∗ (cn ), resulting in total space usage bounded by O∗ (min(cn , 2|H| )). We obtain the following theorem.

Theorem 7. (⋆) Let Γ be a constraint language where SAT(Γ) is sparsely enumerable in O∗ (cn ) time. Then ABD(Γ) is solvable in O∗ (cn ) time and O∗ (min(cn , 2|H| )) space.

3.2 Faster Algorithms for P-ABD

In this section we present improved algorithms for brute force and enumeration for positive abduction, that have the same complexities as the symmetric variants described above. Recall that the baseline bound to beat for P-ABD (from Theorem 3) is O∗ (3n ), and we begin by lowering this to O∗ (2n ) via a more sophisticated exhaustive search scheme.

Algorithm 1 Algorithm A for P-ABD(Γ).

Require: KB,H,M,D, δ 1: E =D∪ δ 2: G = E ∪ {¬x | x ∈ H -E} 3: if KB∧G∧¬M is satisfiable then 4: return ⊥ 5: if KB∧G is satisfiable then 6: return ⊤ 7: else 8: if D = ∅ then 9: return ⊥ 10: flag = ⊥ 11: for x ∈ D do 12: flag = flag ∨ A(KB, H, M, D - {x}, δ) 13: δ = δ ∪ {x} 14: return flag

Proof. Consider Algorithm 1. The starting parameters are D = H and δ = ∅. The recursive algorithm systematically explores all subsets of H as candidates. It starts with the base candidate E = H. Inside each recursive call, it first checks if the current candidate E, extended to a full candidate G, entails the manifestation (line 3). If this fails, it concludes that neither G nor any subset of G (which includes E and all its subsets) can be an explanation, and returns ⊥. Else, it checks if G is consistent with KB. If yes, then G is obviously a (full) explanation, but the algorithm concludes that in this case even E ⊆ G is a (positive) explanation. If G is not consistent with KB, the algorithm concludes that neither E is consistent with KB, and can thus not be an explanation. Then the algorithm systematically checks candidates where exactly one variable is removed from E (lines 11-14). Descending in the recursive calls (line 12) it makes sure to systematically explore all subsets of a candidate, thereby avoiding visiting the same subset multiple times (this is the purpose of δ). For correctness, we refer to the technical report.

We now consider an algorithm based on enumerating all models of the knowledge base, similar to the symmetric abduction case, by trading polynomial for exponential space.

Theorem 9. (⋆) Let Γ be a constraint language where SAT(Γ) is sparsely enumerable in O∗ (cn ) time. Then P-ABD(Γ) is solvable in O∗ (cn ) time and O∗ (cn ) space.

3.3 Provably Sparse Languages

We have proved that (P-)ABD can be solved faster if all models of the underlying SAT problem can be enumerated sufficiently fast. Hence, it is highly desirable to classify the SAT problems where this is indeed the case - provided that any positive, non-trivial examples actually exist. We obtain a general characterization of such languages based on three abstract properties. Here, we always assume that a SAT(Γ) instance is represented by listing all tuples in a relation.

Definition 10. A constraint language Γ is asymptotically sparse if there exists r0 ≥ 1 and c < 2 such that for r-ary R ∈ Γ, r0 ≤ r we have |R| ≤ cr .

If R is an n-ary relation and g : [m] → [n], for some m ≤ n, then the relation Rg(x1, . . . , xm) ≡ R(xg(1), . . . , xg(m)) is said to be a minor of R.

Definition 11. For a constraint language Γ we let Min(Γ) = {M | M is a minor of R ∈ Γ} be the set of minors of Γ.

Similarly, if R ∈ Γ of arity ar(R) = k and f : X → {0, 1} for some X ⊆ [k] then we define the substitution of f over R as the relation R|f = {Proj[k]-X(t) | t = (c1, . . . , ck) ∈ R, i ∈ X ⇒ ci = f(i)} where Proj[k]-X(t) denotes the (k - |X|)-ary tuple obtained by only keeping indices in [k] outside X.

Definition 12. A language Γ is said to be closed under branching if it is closed under substitutions, i.e., if R ∈ Γ and f : X → {0, 1} for X ⊆ [ar(R)] then R|f ∈ Γ, and is closed under minors, i.e., Min(Γ) = Γ.

We observe that Γ is finite if and only if Min(Γ) is finite.

Example 13. Any language Γ can be closed under branching simply by repeatedly closing it under minors and substitutions. For example, consider 3-SAT and a positive clause corresponding to the relation R = {0, 1}3 -{(0, 0, 0)}. Then Min({R}) = {R, {0, 1}2 - {(0, 0)},⊤}. If we close R under substitutions then we obtain {{0, 1}2 - {(0, 0)}, ⊤, f} by identifying one or more variable to 0 and {{0, 1}2 , {0, 1}, t} by identifying one or more variable to 1.

Thus, while it is easy to close a language Γ under branching, this process might introduce undesirable relations of the form {0, 1}k which do not enforce any constraints.

Definition 14. A relation R ⊂ {0, 1}k is said to be nontrivial. The relation {0, 1}k is said to be trivial.

By combining these properties we obtain a novel characterization of sparsely enumerable languages.

Theorem 15. (⋆) Let Γ be a constraint language which (1) is asymptotically sparse, (2) is closed under branching, and (3) every R ∈ Γ is non-trivial. Then SAT(Γ) is sparsely enumerable.

We continue by proving that such languages actually exist. First, say that a k-ary Boolean relation R is totally symmetric, or just symmetric, if there exists a set S ⊆ [k] ∪{0} such that (x1, . . . , xk) ∈ R if and only if x1+. . .+xk ∈ S. Given S ⊆ {0, . . . , k} we write RS for the symmetric relation induced by S, i.e., RS(x1, . . . , xk) ≡ (∑ xi ∈ S).

Definition 16. We let EQUATIONS = {RS | k ≥ 1, p, q ≤ k + 1, S = {i ∈ [k] ∪ {0} | i ≡ q (mod p)}.

Thus, each relation in EQUATIONS can be defined by an equation of the form x1 + . . . + xk = q (mod p) for fixed p, q, k. In particular AFF ⊆ EQUATIONS but it also contains relations inducing ΣP2 -complete (P-)ABD problems. Perhaps contrary to intuition, EQUATIONS is not closed under minors, since the resulting relations are not necessarily symmetric, but a simple work-around is to fix a finite subset of EQUATIONS and then close it under minors. We obtain the following.

Lemma 17. (⋆) The following statements are true.

1. EQUATIONS is closed under substitutions and contains only non-trivial relations.
2. Let k ≥ 1. For E ≤k = {R ∈ EQUATIONS | ar(R) ≤ k} SAT(Min(E ≤k )) is sparsely enumerable.

Finally, let XSAT ⊆ EQUATIONS be the set of relations R1/k representable by equations x1 + . . . + xk = 1 (mod k) + 1, and for each k ≥ 1 the constant relation ⊥k = {(0, . . . , 0)} of arity k (note also that R1/1 = ⊤), and, finally, the two nullary relations f and t. The resulting problem SAT(XSAT) is thus the natural generalization of the well-known NP-complete problem 1-IN-3-SAT to arbitrary arities. Also, recall that AFF ⊆ EQUATIONS is the set of relations representable by systems of Boolean equations modulo 2, i.e., x1 + . . . + xk ≡ q (mod 2) for q ∈ {0, 1}. We additionally write AFF≤k for the set of affine relations of arity at most k.

Theorem 18. (⋆) The following statements are true.

1. SAT(XSAT) is sparsely enumerable in O∗ (√2n ) time.
2. SAT(AFF≤k ) is sparsely enumerable for every k ≥ 1.

Let us also observe that the bound for SAT(XSAT) is tight in the sense that |Mod(φ)| = √2n , n = 2m, if φ encodes inequalities between x1 and x2, x3 and x4, and so on.

3.4 Algorithms for NP-complete Fragments

Symmetric abduction is NP-complete for k-CNF+ languages for any k ≥ 2, and both symmetric and positive abduction are NP-complete for languages of the form k-CNF-∪ IMP, k ≥ 2 [Nordh and Zanuttini, 2008]. We show in the following that these cases can be solved in improved time.

Definition 19. Denote by SIMPLESATp the SAT-problem where we are given a formula φ of the following form. Here, C stands for a positive clause of size at most p and T stands for a negative term of any size.

Lemma 20. SIMPLESATp can be solved in time O∗ (cn ), where c is the branching factor associated with a (1, . . . , p)- branching.

Proof. Perform a branch and reduce scheme. Variables not occurring in any positive clause can be reduced to 0 (thereby simplifying some of the negative terms). Then branch on the variables of positive clauses, with the standard (1, . . . , p)- branching.

We are now ready to show that ABD(k-CNF+) can be CVreduced to SIMPLESATk .

Theorem21. (⋆) ABD(k-CNF+)≤CV SIMPLESATk . Moreover, the SIMPLESAT-instance contains only variables from H.

We show that (P-)ABD(k-CNF- ∪ IMP) can be CVreduced to ABD(k-CNF+).

The following corollary finally states the improved results, following immediately from the previous statements.

Corollary 23. ABD(k-CNF+) and (P-)ABD(k-CNF- ∪ IMP) can be solved in improved time. That is, in time O∗ (c|H| ), for a c < 2, stemming from the branching vector (1, . . . , k).

3.5 Algorithms for coNP-complete Fragments

In the case of positive abduction coNP-complete cases arise [Nordh and Zanuttini, 2008] when Γ is 1-valid. Under certain additional assumptions, P-ABD(Γ) can then be solved in improved time.

Theorem 24. Let Γ be a 1-valid constraint language. If SAT(Γ+) can be decided in O∗ (cn ) time for c ≤ 2 then P-ABD(Γ) can be decided in O∗ (cn ) time.

Proof. First, note that the 1-valid property is responsible for coNP-membership: there is an explanation iff H is an explanation. Then KB ∧ H is always consistent (since 1-valid). Thus, we only need to check whether KB ∧ H |= M. This implication can be decided by invoking the given SAT(Γ+) algorithm |M| times: KB ∧ H |= M iff for each m ∈ M the Γ+-formula KB ∧ H ∧ ¬m is unsatisfiable, and we thus only increase the O∗ (cn ) complexity by a polynomial factor.

An application example is a knowledge base in k-CNF (k ≥ 3) where each clause contains at least 1 positive literal (this ensures 1-validity). The underlying constraint language Γ is still expressive enough to render P-ABD(Γ) coNP-hard [Nordh and Zanuttini, 2008]. Then, any Γ+-formula is expressible as k-CNF formula (without additional variables), so SAT(Γ+) can be solved in improved time via the standard (1, . . . , k)-branching. With Theorem 24 we conclude that P-ABD(Γ) can be solved in improved time.

4 Lower Bounds and Reductions

We continue by matching our new upper bounds with lower bounds. We base our lower bounds on ETH and its stronger variant SETH (recall the definition in Section 1).

4.1 ETHBased Lower Bounds

Our aim in this section is to prove the following theorem.

Proof. We provide a CV-reduction from the k-colored clique problem to ABD(2-CNF- ∪ IMP), i.e., given a graph G = (V, E) where the vertices are colored with k different colors, decide if a clique containing a vertex of each color exists. It is known that k-colored clique cannot be solved in time ( nk )o(k) under ETH, where n is the number of vertices, and k is the number of colors [Lokshtanov et al., 2011].

For the reduction, assume an arbitrary instance of a kcolored clique problem over a graph G = (V, E), and where C = ci | i ∈ [1 . . . k] is the set of colors. For each color ci we add a manifestation mi to M. For each vertex vi colored with the color ci we add to KB the clause (¬vi ∨mi). For each two vertices vi and vj that are not connected by an edge, we add the clause (¬vi ∨ ¬vj). This completes the reduction. Since the number of variables in the abduction problem is equal to the number of vertices plus the number of colors, this is a CVreduction. If we can choose a clique that contains at least one vertex from each color without choosing two vertices that are not connected, then for each chosen vertex vi, we set vi = ⊤ in the abduction instance as part of the solution. This will entail all mi's without causing a contradiction in KB. The correctness proof from the other side is exactly the same.

Note that this lower bound is given with respect to |H| and |M| and not n, and it is identical to the running time of the brute force algorithms of these problems. Indeed, in the worst case, we try all possible combinations of hypotheses for all manifestations. If a hypothesis appears for two manifestations at the same time, it only reduces the need to choose an additional hypothesis for the second one. The worst case is then when all hypotheses are split up among manifestations. The number of combinations is thus ( |H| |M| )|M| , making the algorithm close to optimal.

4.2 Lower Bounds for (P-)ABD(4-CNF) under SETH

Here, we prove a strong lower bound under SETH which shows that we should only expect small improvements for 4-CNF, and, more generally, k-CNF for any k ≥ 4.

Theorem 26. (⋆) Under SETH, there is no c < 1 such that ABD(4-CNF) is solvable in 2cn time.

The following lemma gives the slightly worse lower bound for positive abduction variant of 4-CNF.

Lemma 27. (⋆) Under SETH, there is no c < 1 such that P-ABD(4-CNF) can be solved in time 1.4142cn .

We remark that this leaves 3-CNF as an interesting open case. We have no algorithms that run in less than 2n so far, and no known lower bounds under SETH.

4.3 Languages Closed under Complement

We analyze languages closed only under complement, i.e., languages Γ such that Pol(Γ) = [¯x]. Well-known examples of such languages include not-all-equal satisfiability. For this class of languages we manage to relate them to languages closed only under projections, in a very precise sense, and show that one without loss of generality can concentrate solely on the latter class.

Theorem 28. (⋆) Let Γ be a constraint language such that Pol(Γ) = [¯x]. Then (P-)ABD(Γ ∪ {⊥,⊤}) =CV (P-)ABD(Γ).

For the next theorem, let k-NAE be the set of all k-ary relations that forbid exactly two complementary assignments (determined by a sign pattern). The full details can be found in the technical report.

Thus, in general we should not expect to solve complementative abduction problems faster than 2n (via Theorem 26).

4.4 Lower Bounds for Horn and CNF+ Abduction

Last, we prove strong lower bounds for Horn and CNF+. These lower bounds do not conclusively rule out algorithms faster than 2n but we stress that sharp lower (under SETH) and upper bounds of the form cn are rather uncommon in the literature, and an improved upper bound would likely need to use completely new ideas.

Lemma 30. (⋆) Under SETH, there is no c < 1 such that (P-)ABD(CNF- ∪ IMP) can be solved in time 1.2599cn or

.

Since 2-CNF- ∪ IMP is a special case of Horn, we obtain the same lower bounds for Horn knowledge bases. Furthermore, using the reduction from Lemma 22, we obtain a CVreduction from (P-)ABD(CNF- ∪ IMP) to ABD(CNF+), and CNF+ in turn is a special case of DualHorn. We therefore obtain the following Corollary.

Corollary 31. Under SETH, there is no c < 1 such that (P)ABD(Horn) as well as ABD(CNF+) and ABD(DualHorn) can be solved in time 1.2599cn or 1.4142c|H| or 2c|M| or ( |H| |M| )c|M| .

An interesting question that might occur is whether or not we can have SETH lower bounds for the problems in Section 4.1. Those problems instead have weaker lower bounds from ETH. The following lemma will show that we are unlikely to obtain such bounds with the same method we obtained them for the problems in this Section (4.4).

Proof. We provide a short proof sketch. From [Fortnow and Santhanam, 2011], we know that CNF-SAT does not admit a kernel of size f(n) where f is a polynomial, i.e., an equisatisfiable instance with e.g. a quadratic number of clauses (unless NP ⊆ P/Poly). To prove the claim it suffices to have a reduction from ABD(2-CNF) to CNF-SAT that only has a polynomial number of clauses in terms of n. Assume an arbitrary ABD(2-CNF) instance. For every mi ∈ M, for all clauses of the type: (ℓj ∨mi), . . . , (ℓk ∨mi) where ℓi . . . ℓk are a literals, we delete these clauses and add the following CNF clause (ℓi ∨ . . . ∨ ℓk), and otherwise keep everything unchanged.

It is thus unlikely to obtain SETH lower bounds for ABD(2-CNF) from CNF-SAT under LV- or CV-reductions.

5 Concluding Remarks

We demonstrated that non-monotonic reasoning, and in particular propositional abduction, for many non-trivial cases do admit improvements over exhaustive search. We find it particularly interesting that even ΣP2 -complete problems fall under the scope of our methods. Might it even be the case that ΣP2 is not such an imposing barrier as classical complexity theory tells us? Nevertheless, despite many positive and negative results, there are still open cases remaining and many interesting directions for future research.

Faster Enumeration? We proved that finite subsets of AFF and EQUATIONS are susceptible to enumeration. It is easy to see that Pol(AFF) contains the Maltsev operation x - y + z( (mod 2)), while EQUATIONS is exactly the set of symmetric relations invariant under a partial Maltsev operation [Lagerkvist andWahlstr¨om, 2022]. Is it a coincidence that all of our positive enumeration cases can be explained by partial Maltsev operation, or could universal algebra be applied even further? For example, it is straightforward to show that if a language is not preserved by partial Maltsev, then it can not be sparsely enumerable. Extending this further, if one allows e.g. a polynomial-time preprocessing, could it even be the case that a Boolean (possibly non-symmetric) language is sparsely enumerable if and only if it is invariant under partial Maltsev?

2- and 3-CNF. While (P-)ABD(4-CNF) is unlikely to admit improved algorithms, (P-)ABD(k-CNF) for k ≤ 3 is wide open. These languages are not sparsely enumerable so they do not fall under the scope of the enumeration algorithms, yet, it appears highly challenging to prove sharp lower bounds for them (and recall that CNF-SAT does not admit an LV-reduction to (P-)ABD(2-CNF) unless NP ⊆ P/Poly). As a possible starting point one could consider instances with only a linear number m of clauses in the knowledge base, or, the more restricted case when each variable may only occur in a fixed number of constraints. Could instances of this kind be solved with enumeration?

Other Parameters? Related to the above question one could more generally ask when (P-)ABD(Γ) admits an improved algorithm with complexity parameter m, which we observe in general can be much larger than n. Do any of the algorithmic results carry over, and can lower bounds be obtained? For the related quantified Boolean formula problems, Williams [2002] constructed an O(1.709m) time algorithm, so one could be cautiously optimistic about analyzing abduction with m.

Acknowledgements

The authors are supported by the Swedish research council under grant VR-2022-03214.