Abstract
We show a reduction to propositional logic from quantifierfree Presburger arithmetic, and disjunctive linear arithmetic, based on Fourier-Motzkin elimination. While the complexity ofthis procedure is not better than competing techniques, it has practical advantages in solving verification problems. It also promotes the option ofdeciding a combination oftheories by reducing them to this logic.
Cite
CITATION STYLE
Strichman, O. (2002). On solving presburger and linear arithmetic with SAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2517, pp. 160–170). Springer Verlag. https://doi.org/10.1007/3-540-36126-x_10
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
