Deciding Separation Formulas with SAT
journal contributionposted on 01.01.1998 by Ofer Strichman, Sanjit A Seshia, Randal E. Bryant
Any type of content formally published in an academic journal, usually following a peer-review process.
We show a reduction to propositional logic from a Boolean combination of inequalities of the form v i ≥ v j + c and v i > v j + c, where c is a constant and v i, v j 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.