.png){kind=icon}
.png){kind=icon}
Return
Algorithms and complexity of difference logic
.png){kind=icon}
OA
AI
DOI：10.1016/j.jcss.2026.103780.png)
.png){kind=icon}
.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Difference Logic (DL) is a fragment of linear arithmetic 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 analysing 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 generalise our results to integer domains and sentences that are not in CNF.
Keywords:
Difference logic
Algorithms and complexity
Fine-grained complexity
Parameterized complexity
Treewidth
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
J
IF:
0.9
Papers:
51
Citations:
4.5K
View more organizations