Abstract
We present a novel decision procedure for non-linear real arithmetic: a combination of iSAT, an incomplete SMT solver based on interval constraint propagation (ICP), and an implementation of the complete cylindrical algebraic decomposition (CAD) method in the library GiNaCRA . While iSAT is efficient in finding unsatisfiability, on satisfiable instances it often terminates with an interval box whose satisfiability status is unknown to iSAT. The CAD method, in turn, always terminates with a satisfiability result. However, it has to traverse a double-exponentially large search space.
A symbiosis of iSAT and CAD combines the advantages of both methods resulting in a fast and complete solver. In particular, the interval box determined by iSAT provides precious extra information to guide the CAD-method search routine: We use the interval box to prune the CAD search space in both phases, the projection and the construction phase, forming a search “tube” rather than a search tree. This proves to be particularly beneficial for a CAD implementation designed to search a satisfying assignment pointedly, as opposed to search and exclude conflicting regions.
This work has been partially supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “AVACS” (SFB/TR 14, http://www.avacs.org/ and the Research Training Group “AlgoSyn” (GRK 1298, http://www.algosyn.rwth-aachen.de/ )
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Anai, H., Yokoyama, K.: Cylindrical algebraic decomposition via numerical computation with validated symbolic reconstruction. In: Algorithmic Algebra and Logic, pp. 25–30 (2005)
Basu, S., Pollack, R., Roy, M.: Algorithms in Real Algebraic Geometry. Springer (2010)
Benhamou, F., Granvilliers, L.: Continuous and Interval Constraints. In: Handbook of Constraint Programming, pp. 571–603. Foundations of Artificial Intelligence (2006)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58, 118–149 (2003)
Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)
Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5, 394–397 (1962)
Eggers, A., Kruglov, E., Kupferschmid, S., Scheibler, K., Teige, T., Weidenbach, C.: Superposition modulo non-linear arithmetic. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 119–134. Springer, Heidelberg (2011)
Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling, and Computation 1(3-4), 209–236 (2007)
Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: ISSAC 1990, pp. 261–264. ACM (1990)
Iwane, H., Yanami, H., Anai, H.: An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for optimization problems. In: Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation, pp. 168–177. ACM (2012)
Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339–354. Springer, Heidelberg (2012)
Mishra, B.: Algorithmic Algebra. Texts and Monographs in Computer Science. Springer (1993)
Ratschan, S.: Approximate quantified constraint solving by cylindrical box decomposition. Reliable Computing 8(1), 21–42 (2002)
Silva, J.P.M., Sakallah, K.A.: Grasp - a new search algorithm for satisfiability. In: ICCAD, pp. 220–227 (1996)
Strzebonski, A.W.: Cylindrical algebraic decomposition using validated numerics. Journal of Symbolic Computation 41(9), 1021–1038 (2006)
Tseitin, G.S.: On the complexity of derivations in propositional calculus. In: Slisenko, A. (ed.) Studies in q(1968)
Weispfenning, V.: The complexity of linear problems in fields. Journal of Symbolic Computation 5(1-2), 3–27 (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Loup, U., Scheibler, K., Corzilius, F., Ábrahám, E., Becker, B. (2013). A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition. In: Bonacina, M.P. (eds) Automated Deduction – CADE-24. CADE 2013. Lecture Notes in Computer Science(), vol 7898. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38574-2_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-38574-2_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38573-5
Online ISBN: 978-3-642-38574-2
eBook Packages: Computer ScienceComputer Science (R0)