Difference logic

also: bellman-ford, negative cycle

The fragment of linear arithmetic whose atoms all have the form x - y <= k. A set of such constraints is a weighted graph, and it is satisfiable exactly when the graph has no negative cycle, so Bellman-Ford both decides it and, on failure, hands back the cycle as the explanation.

The fragment of linear arithmetic in which every atom has the shape

It is weak enough to decide in polynomial time and strong enough for scheduling, timing analysis, and most of what a bounded model checker generates.

The decision procedure is a graph algorithm. Make a vertex per variable and an edge $y\stackrel{k}{\to }x$ for each constraint $x-y\le k$. A path spells out a chain of inequalities, so a cycle of total weight $w$ says $x-x\le w$, which is a contradiction exactly when $w<0$.

Bellman-Ford decides that in $O(VE)$ and, on failure, hands back the cycle itself. That cycle is a minimal conflicting subset of the constraints, which is precisely the explanation DPLL(T) wants, so the theory solver gets its explanation for free rather than having to reconstruct one. A satisfying assignment reads off the same run as the shortest-path distances from a virtual source connected to every vertex with weight zero.

Theory solver · SMT

• Implementing SAT in OCaml Part 4A real linear-arithmetic fragment: difference logic atoms x - y <= k, decided by Bellman-Ford negative-cycle detection with explanations.