## 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: | 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. |

Pages: | 14 |

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

Paper: |