Computer Science Department
School of Computer Science, Carnegie Mellon University
Reducing Separation Formulas to Propositional Logic
Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant
April 2002
CMU-CS-02-132.ps
CMU-CS-02-132.pdf
A short version of this report titled, Deciding
Separation Formulas with SAT
appeared in the Proceedings of the 14th International Conference
on
Computer Aided Verification, Copenhagen, Denmark, July 2002.
We show a reduction to propositional logic from a Boolean combination
of inequalities of the form x >= y + c and x > y + c,
where c is a constant and x,y 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.
21 pages
Return to:
SCS Technical Report Collection This page maintained by [email protected]
School of Computer Science homepage