Algorithms and Complexity of Difference Logic
| Autor: | Dabrowski, Konrad K., Jonsson, Peter, Ordyniak, Sebastian, Osipov, George |
|---|---|
| Rok vydání: | 2024 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: This is an strongly extended version of two conference papers with the same authors that appeared at KR 2020 (Title: Fine-Grained Complexity of Temporal Problems) and AAAI 2021 (Title: Disjunctive Temporal Problems under Structural Restrictions) |
| Databáze: | arXiv |
| Externí odkaz: |
|