Fast and Flexible Difference Constraint Propagation for DPLL(T)

摘要

In the context of DPLL(T), theory propagation is the process of dynamically selecting consequences of a conjunction of constraints from a given set of candidate constraints. We present improvements to a fast theory propagation procedure for difference constraints of the form x — y ≤ c. These improvements are demonstrated experimentally.