The potential and challenges of CAD with equational constraints for SC-square

James H. Davenport, Matthew England

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Cylindrical algebraic decomposition (CAD) is a core algorithm within Symbolic Computation, particularly for quantifier elimination over the reals and polynomial systems solving more generally. It is now finding increased application as a decision procedure for Satisfiability Modulo Theories (SMT) solvers when working with non-linear real arithmetic. We discuss the potentials from increased focus on the logical structure of the input brought by the SMT applications and SC 2 project, particularly the presence of equational constraints. We also highlight the challenges for exploiting these: primitivity restrictions, well-orientedness questions, and the prospect of incrementality.

Original languageEnglish
Title of host publicationMathematical Aspects of Computer and Information Sciences - 7th International Conference, MACIS 2017, Proceedings
Place of PublicationGermany
PublisherSpringer Verlag
Pages280-285
Number of pages6
ISBN (Print)9783319724522
DOIs
Publication statusPublished - 2017
Event7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017 - Vienna, Austria
Duration: 15 Nov 201717 Nov 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10693

Conference

Conference7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017
CountryAustria
CityVienna
Period15/11/1717/11/17

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'The potential and challenges of CAD with equational constraints for SC-square'. Together they form a unique fingerprint.

Cite this