General overview of a T-Solver for Difference Logic https://www.cs.upc.edu/~oliveras/TDV/dl.pdf グラフの経路探索アルゴリズムであるBellman-Fordが、どうして difference logic という算術の問題を解くのに使われるのか、昔からちょっとだけ気になっていたけれど、そういうことだったのね。 分かりやすくまとまっているスライド。