  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.
