以前に紹介[1]した General overview of a T-Solver for Difference Logic [2]で、Theory Propagation の実装がよく分かっていなかったが、Fast and Flexible Difference Constraint Propagation for DPLL(T) [3]にはその辺り詳しく書いてそう。
[1] https://plus.google.com/+MasahiroSakai/posts/YmtVNUpg5Gi
[2] General overview of a T-Solver for Difference Logic
https://www.cs.upc.edu/~oliveras/TDV/dl.pdf
[3] Fast and Flexible Difference Constraint Propagation for DPLL(T)
http://www-verimag.imag.fr/~maler/Papers/slides-dlsat.pdf
http://www-verimag.imag.fr/~maler/Papers/ffdcp.pdf