Table of Contents
Fetching ...

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

Victor Lagerkvist, Mohamed Maizia, Johannes Schmidt

TL;DR

The paper addresses the fine-grained complexity of propositional abduction, focusing on ABD and P-ABD under the natural parameter $n$, the number of variables. It develops SAT-based upper bounds and identifies sparsely enumerable constraint languages (e.g., Equations, XSAT, AFF) that enable faster algorithms, including beating exhaustive search for certain $\Sigma^P_2$-complete cases. It introduces a unifying sparsity framework and reductions to structured SAT problems (like SimpleSAT$^p$) to derive improved bounds for NP-complete and coNP-complete fragments, while simultaneously establishing ETH/SETH-based lower bounds that rule out many subexponential improvements. The results illuminate when non-monotonic reasoning via abduction can be solved faster than naive enumeration and reveal connections to algebraic structures (e.g., partial Maltsev operations) and constraint language theory, with implications for explainability in AI systems.

Abstract

The Boolean satisfiability problem (SAT) is a well-known example of monotonic reasoning, of intense practical interest due to fast solvers, complemented by rigorous fine-grained complexity results. However, for non-monotonic reasoning, e.g., abductive reasoning, comparably little is known outside classic complexity theory. In this paper we take a first step of bridging the gap between monotonic and non-monotonic reasoning by analyzing the complexity of intractable abduction problems under the seemingly overlooked but natural parameter n: the number of variables in the knowledge base. We obtain several positive results for $Σ^P_2$- as well as NP- and coNP-complete fragments, which implies the first example of beating exhaustive search for a $Σ^P_2$-complete problem (to the best of our knowledge). We complement this with lower bounds and for many fragments rule out improvements under the (strong) exponential-time hypothesis.

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

TL;DR

The paper addresses the fine-grained complexity of propositional abduction, focusing on ABD and P-ABD under the natural parameter , the number of variables. It develops SAT-based upper bounds and identifies sparsely enumerable constraint languages (e.g., Equations, XSAT, AFF) that enable faster algorithms, including beating exhaustive search for certain -complete cases. It introduces a unifying sparsity framework and reductions to structured SAT problems (like SimpleSAT) to derive improved bounds for NP-complete and coNP-complete fragments, while simultaneously establishing ETH/SETH-based lower bounds that rule out many subexponential improvements. The results illuminate when non-monotonic reasoning via abduction can be solved faster than naive enumeration and reveal connections to algebraic structures (e.g., partial Maltsev operations) and constraint language theory, with implications for explainability in AI systems.

Abstract

The Boolean satisfiability problem (SAT) is a well-known example of monotonic reasoning, of intense practical interest due to fast solvers, complemented by rigorous fine-grained complexity results. However, for non-monotonic reasoning, e.g., abductive reasoning, comparably little is known outside classic complexity theory. In this paper we take a first step of bridging the gap between monotonic and non-monotonic reasoning by analyzing the complexity of intractable abduction problems under the seemingly overlooked but natural parameter n: the number of variables in the knowledge base. We obtain several positive results for - as well as NP- and coNP-complete fragments, which implies the first example of beating exhaustive search for a -complete problem (to the best of our knowledge). We complement this with lower bounds and for many fragments rule out improvements under the (strong) exponential-time hypothesis.
Paper Structure (37 sections, 22 theorems, 11 equations, 2 figures, 2 tables, 4 algorithms)

This paper contains 37 sections, 22 theorems, 11 equations, 2 figures, 2 tables, 4 algorithms.

Key Result

Theorem 3

($\star$) Let $\Gamma$ be a constraint language such that $\textsc{SAT}(\Gamma^+)$ is solvable in $f(n)$ time for some computable function $f \colon \mathbb{N} \to \mathbb{N}$. Then

Figures (2)

  • Figure 1: Classical complexity of ABD according to Nordh and Zanuttini (2008), illustrated on Post's lattice.
  • Figure 2: Classical complexity of P-ABD according to Nordh and Zanuttini (2008), illustrated on Post's lattice.

Theorems & Definitions (60)

  • Example 1
  • Definition 2
  • Theorem 3
  • Definition 4
  • Definition 5
  • Lemma 6
  • Theorem 7
  • Theorem 8
  • proof
  • Theorem 9
  • ...and 50 more