An extension of the Davis-Putnam procedure and its application to preprocessing in SMT
Roberto Bruttomesso · 2009
We present a decision procedure for SMT(LRA) that works by eliminating Boolean and rational variables. The algorithm we propose (DPFM) is based on a combination of the Davis-Putnam procedure and the Fourier-Motzkin elimination. We report on preliminary experiments where DPFM is not directly used to solve the formula (as its prohibitive complexity does not make it practical), but it is instead used in a controlled manner as a simplification and preprocessing device.