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 proceeding

4 Downloads (Pure)

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-Square 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 (Proc. MACIS '17)
Subtitle of host publicationMACIS 2017
PublisherSpringer
Pages280-285
Number of pages6
VolumeLNCS 10693
ISBN (Electronic)978-3-319-72453-9
ISBN (Print)978-3-319-72452-2
DOIs
Publication statusPublished - 21 Dec 2017
Event7th International Conference on Mathematical Aspects of Computer and Information Sciences - Vienna, Austria
Duration: 15 Nov 201717 Nov 2017
Conference number: 7
https://macis2017.sba-research.org/

Publication series

NameLecture Notes in Computer Science (LNCS)
PublisherSpringer

Conference

Conference7th International Conference on Mathematical Aspects of Computer and Information Sciences
Abbreviated titleMACIS 2017
CountryAustria
CityVienna
Period15/11/1717/11/17
Internet address

Fingerprint

Decomposition
Polynomials

Bibliographical note

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-72453-9_22

Cite this

Davenport, J. H., & England, M. (2017). The Potential and Challenges of CAD with Equational Constraints for SC-Square. In Mathematical Aspects of Computer and Information Sciences (Proc. MACIS '17): MACIS 2017 (Vol. LNCS 10693, pp. 280-285). (Lecture Notes in Computer Science (LNCS)). Springer. https://doi.org/10.1007/978-3-319-72453-9_22

The Potential and Challenges of CAD with Equational Constraints for SC-Square. / Davenport, James H.; England, Matthew.

Mathematical Aspects of Computer and Information Sciences (Proc. MACIS '17): MACIS 2017. Vol. LNCS 10693 Springer, 2017. p. 280-285 (Lecture Notes in Computer Science (LNCS)).

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

Davenport, JH & England, M 2017, The Potential and Challenges of CAD with Equational Constraints for SC-Square. in Mathematical Aspects of Computer and Information Sciences (Proc. MACIS '17): MACIS 2017. vol. LNCS 10693, Lecture Notes in Computer Science (LNCS), Springer, pp. 280-285, 7th International Conference on Mathematical Aspects of Computer and Information Sciences, Vienna, Austria, 15/11/17. https://doi.org/10.1007/978-3-319-72453-9_22
Davenport JH, England M. The Potential and Challenges of CAD with Equational Constraints for SC-Square. In Mathematical Aspects of Computer and Information Sciences (Proc. MACIS '17): MACIS 2017. Vol. LNCS 10693. Springer. 2017. p. 280-285. (Lecture Notes in Computer Science (LNCS)). https://doi.org/10.1007/978-3-319-72453-9_22
Davenport, James H. ; England, Matthew. / The Potential and Challenges of CAD with Equational Constraints for SC-Square. Mathematical Aspects of Computer and Information Sciences (Proc. MACIS '17): MACIS 2017. Vol. LNCS 10693 Springer, 2017. pp. 280-285 (Lecture Notes in Computer Science (LNCS)).
@inproceedings{9a6157d23b8a468194cd67d08bdef0e6,
title = "The Potential and Challenges of CAD with Equational Constraints for SC-Square",
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-Square 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.",
author = "Davenport, {James H.} and Matthew England",
note = "The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-72453-9_22",
year = "2017",
month = "12",
day = "21",
doi = "10.1007/978-3-319-72453-9_22",
language = "English",
isbn = "978-3-319-72452-2",
volume = "LNCS 10693",
series = "Lecture Notes in Computer Science (LNCS)",
publisher = "Springer",
pages = "280--285",
booktitle = "Mathematical Aspects of Computer and Information Sciences (Proc. MACIS '17)",

}

TY - GEN

T1 - The Potential and Challenges of CAD with Equational Constraints for SC-Square

AU - Davenport, James H.

AU - England, Matthew

N1 - The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-72453-9_22

PY - 2017/12/21

Y1 - 2017/12/21

N2 - 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-Square 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.

AB - 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-Square 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.

U2 - 10.1007/978-3-319-72453-9_22

DO - 10.1007/978-3-319-72453-9_22

M3 - Conference proceeding

SN - 978-3-319-72452-2

VL - LNCS 10693

T3 - Lecture Notes in Computer Science (LNCS)

SP - 280

EP - 285

BT - Mathematical Aspects of Computer and Information Sciences (Proc. MACIS '17)

PB - Springer

ER -