Evaluation of Equational Constraints for CAD in SMT Solving

Authors: Rebecca Haehn, Gereon Kremer and Erika Ábrahám

Paper Information

Title:Evaluation of Equational Constraints for CAD in SMT Solving
Authors:Rebecca Haehn, Gereon Kremer and Erika Ábrahám
Proceedings:SCSC Papers
Editors: Anna Maria Bigatti and Martin Brain
Keywords:cylindrical algebraic decomposition, equational constraints, SMT solving

ABSTRACT. The cylindrical algebraic decomposition is a popular method for quantifier elimination for non-linear real algebra. We use it as a theory solver in the context of satisfiability-modulo-theories solving to solve a sequence of related problems consisting of a conjunction of constraints. To improve our technique in practice, we consider different optimizations in the projection phase based on equational constraints.

We review the existing ideas and propose how to modify an existing implementation. Though one could expect a significant speed-up for large problems, we discuss why our expectations are somewhat lower, in particular, because satisfiable problems tend not to benefit from the modifications at all. Finally, we evaluate several different implementations and demonstrate a significant improvement due to the usage of equational constraints.

Talk:Jul 11 15:00 (Session 66D: Research papers: CAD)