Algorithms and Complexity of Difference Logic
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866909093938069504 |
|---|---|
| author | Dabrowski, Konrad K. Jonsson, Peter Ordyniak, Sebastian Osipov, George |
| author_facet | Dabrowski, Konrad K. Jonsson, Peter Ordyniak, Sebastian Osipov, George |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_03273 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Algorithms and Complexity of Difference Logic Dabrowski, Konrad K. Jonsson, Peter Ordyniak, Sebastian Osipov, George Data Structures and Algorithms Logic in Computer Science 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. |
| title | Algorithms and Complexity of Difference Logic |
| topic | Data Structures and Algorithms Logic in Computer Science |
| url | https://arxiv.org/abs/2402.03273 |