Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Algorithms and Complexity of Difference Logic

Konrad K. Dabrowski, Peter Jonsson, Sebastian Ordyniak, George Osipov

TL;DR

The paper conducts a thorough fine-grained complexity study of Difference Logic (DL) satisfiability, focusing on existential CNF sentences over rational variables and analyzing time complexity and parameterized complexity under arity and coefficient bounds. It establishes tight ETH-based upper and lower bounds for various restricted CSP languages ${\bf D}_{a,k}$, proves XP algorithms under incidence-treewidth for DL fragments, and demonstrates W[1]-hardness and pNP-hardness for key subproblems via reductions from Subset Sum, independent-set variants, and the multi-dimensional Subset Sum problem. A central technical contribution is the small-solution property for ${\sc CSP}({\bf D})$ enabling compact encodings, together with a novel divide-and-conquer strategy that yields a $2^{O(n\log\log n)}$ time algorithm for ${\sc CSP}({\bf D}_{2,k})$. The work also extends results to non-CNF formulas and to integer domains, enhancing the understanding of the DL-SAT landscape and guiding future inquiries into more general DL formalisms and structural parameterizations. Overall, the findings delineate when DL satisfiability remains tractable under strong complexity hypotheses and when natural restrictions still inherit hardness, informing practical SMT and AI applications that rely on DL reasoning.

Abstract

Difference Logic (DL) is a fragment of linear arithmetics where atoms are constraints x+k <= y for variables x,y (ranging over Q or Z) and integer k. We study the complexity of deciding the truth of existential DL sentences. This problem appears in many contexts: examples include verification, bioinformatics, telecommunications, and spatio-temporal reasoning in AI. We begin by considering sentences in CNF with rational-valued variables. We restrict the allowed clauses via two natural parameters: arity and coefficient bounds. The problem is NP-hard for most choices of these parameters. As a response to this, we refine our understanding by analyzing the time complexity and the parameterized complexity (with respect to well-studied parameters such as primal and incidence treewidth). We obtain a comprehensive picture of the complexity landscape in both cases. Finally, we generalize our results to integer domains and sentences that are not in CNF.

Algorithms and Complexity of Difference Logic

TL;DR

The paper conducts a thorough fine-grained complexity study of Difference Logic (DL) satisfiability, focusing on existential CNF sentences over rational variables and analyzing time complexity and parameterized complexity under arity and coefficient bounds. It establishes tight ETH-based upper and lower bounds for various restricted CSP languages , proves XP algorithms under incidence-treewidth for DL fragments, and demonstrates W[1]-hardness and pNP-hardness for key subproblems via reductions from Subset Sum, independent-set variants, and the multi-dimensional Subset Sum problem. A central technical contribution is the small-solution property for enabling compact encodings, together with a novel divide-and-conquer strategy that yields a time algorithm for . The work also extends results to non-CNF formulas and to integer domains, enhancing the understanding of the DL-SAT landscape and guiding future inquiries into more general DL formalisms and structural parameterizations. Overall, the findings delineate when DL satisfiability remains tractable under strong complexity hypotheses and when natural restrictions still inherit hardness, informing practical SMT and AI applications that rely on DL reasoning.

Abstract

Difference Logic (DL) is a fragment of linear arithmetics where atoms are constraints x+k <= y for variables x,y (ranging over Q or Z) and integer k. We study the complexity of deciding the truth of existential DL sentences. This problem appears in many contexts: examples include verification, bioinformatics, telecommunications, and spatio-temporal reasoning in AI. We begin by considering sentences in CNF with rational-valued variables. We restrict the allowed clauses via two natural parameters: arity and coefficient bounds. The problem is NP-hard for most choices of these parameters. As a response to this, we refine our understanding by analyzing the time complexity and the parameterized complexity (with respect to well-studied parameters such as primal and incidence treewidth). We obtain a comprehensive picture of the complexity landscape in both cases. Finally, we generalize our results to integer domains and sentences that are not in CNF.
Paper Structure (33 sections, 38 theorems, 42 equations, 4 figures, 3 tables, 1 algorithm)

This paper contains 33 sections, 38 theorems, 42 equations, 4 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. Time Complexity
  4. Parameterized Complexity
  5. Outline
  6. Preliminaries
  7. Difference Logic
  8. Constraint Satisfaction
  9. Sidon Sets
  10. Upper Bounds on Time Complexity
  11. Upper Bound for $\textsc{CSP}({\bf D}\xspace)$
  12. Upper Bound for Lg
  13. Certificates
  14. Instances with Bounded Span
  15. Divide-and-Conquer Strategy
  16. ...and 18 more sections

Key Result

Theorem 1

$\textsc{CSP}({\bf D}\xspace_{3,0})$ is solvable in $2^{O(n)}$ but not in $2^{o(n)}$ time (if the ETH is true).

Figures (4)

  • Figure 1: A graph (left) and an optimal tree decomposition of the graph (right).
  • Figure 2: A tree decomposition (left) and a corresponding nice tree decomposition (right).
  • Figure 3: The board consisting of the bucket part and the garbage part defined in the proof of Theorem \ref{['thm:w1-hard']}. Here, $T_{A} = \sum_{\bar{a} \in A}s(\bar{a})$ for $A \in \{V_1,\dotsc,V_k,E_1,\dotsc,E_K\}$.
  • Figure 4: Possible ways to place the variables $x^{V_i}_{\ell,c}$ and $y^{V_i}_{\ell,c}$ corresponding to the non-zero coordinate $c = (i,j)$ of the $\ell$-th vector $\bar{v}_\ell$ in $V_i$.

Theorems & Definitions (71)

  • Theorem 1: Eriksson:Lagerkvist:ijcai2021
  • Proposition 2
  • Proposition 3
  • Proposition 4: erdos1941problem
  • Lemma 5
  • proof
  • Theorem 6
  • proof
  • Corollary 7
  • proof
  • ...and 61 more