We show a reduction to propositional logic from a Boolean combination of inequalities of the form vi ≥ vj + c and vi > vj + c,where c is a constant and vi, vj are variables of type real or integer. Equalities and uninterpreted functions can be expressed in this logic as well. We discuss the advantages of using this reduction as compared to competing methods, and present experimental results that support our claims.
CITATION STYLE
Strichman, O., Seshia, S. A., & Bryant, R. E. (2002). Deciding separation formulas with SAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2404, pp. 209–222). Springer Verlag. https://doi.org/10.1007/3-540-45657-0_16
Mendeley helps you to discover research relevant for your work.