Algorithms and Complexity of Difference Logic
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要