Abstract
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.
This research was supported in part by the Office of Naval Research (ONR) and the Naval Research Laboratory (NRL) under contract no. N00014-01-1-0796, and the Gigascale Research Center under contract 98-DT-660. The second author is supported in part by a National Defense Science and Engineering Graduate Fellowship.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
W. Ackermann. Solvable cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1954.
B. Barras, S. Boutin, C. Cornes, J. Courant, J. C. Filliatre, E. Giménez, H. Herbelin, G. Huet, C. Munoz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual-Version V6.1. Technical Report RT-0203, INRIA, August 1997. revised version distributed with Coq.
A. J. C. Bik and H. A. G. Wijshoff. Implementation of Fourier-Motzkin elimination. Technical Report 94-42, Dept. of Computer Science, Leiden University, 1994.
R. Bryant, S. German, and M. Velev. Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Transactions on Computational Logic, 2(1):1–41, 2001.
R. E. Bryant, S. K. Lahiri, and S. A. Seshia. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In Proc. Computer-Aided Verification (CAV’02), July 2002. This volume.
T. Cormen, C. Leiserson, and L. Rivest. Introduction to Algorithms.MIT press.
J. Møller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference decision diagrams. In Proceedings 13th International Conference on Computer Science Logic, volume 83 of LNCS, pages 111–125, 1999.
M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proc. Design Automation Conference (DAC’01), 2001.
V. Pratt. Two easy theories whose combination is hard. Technical report, Massachusetts Institute os Technology, 1977. Cambridge, Mass.
R. Shostak. Deciding linear inequalities by computing loop residues. J. ACM, 28(4):769–779, October 1981.
R. Shostak. Deciding combinations of theories. J. ACM, 31(1):1–12, 1984.
O. Strichman. Optimizations in decision procedures for propositional linear inequalities. Technical Report CMU-CS-02-133, Carnegie Mellon University, 2002.
O. Strichman, S. A. Seshia, and R. E. Bryant. Reducing separation formulas to propositional logic. Technical Report CMU-CS-02-132, Carnegie Mellon University, 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Strichman, O., Seshia, S.A., Bryant, R.E. (2002). Deciding Separation Formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45657-0_16
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43997-4
Online ISBN: 978-3-540-45657-5
eBook Packages: Springer Book Archive