An SMT solver for non-linear real arithmetic inside maple

AmirHosein Sadeghimanesh; Matthew England

doi:10.1145/3572867.3572880

An SMT solver for non-linear real arithmetic inside maple

AmirHosein Sadeghimanesh, Matthew England

Research Centre for Computational Science and Mathematical Modelling

Research output: Contribution to journal › Article › peer-review

119 Downloads (Pure)

Abstract

We report on work-in-progress to create an SMT-solver inside Maple for non-linear real arithmetic (NRA). We give background information on the algorithm being implemented: cylindrical algebraic coverings as a theory solver in the lazy SMT paradigm. We then present some new work on the identification of minimal conflicting cores from the coverings.

Original language	English
Pages (from-to)	76-79
Number of pages	4
Journal	ACM Communications in Computer Algebra
Volume	56
Issue number	2
DOIs	https://doi.org/10.1145/3572867.3572880
Publication status	Published - 23 Nov 2022

Bibliographical note

© ACM, 2022. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Communications in Computer Algebra, vol. 56, no. 2, pp. 76-79.http://doi.acm.org/10.1145/3572867.3572880

Keywords

Computer Algebra
Symbolic computation
satisfiability modulo theories
cylindrical algebraic coverings
Set covering problem

Access to Document

10.1145/3572867.3572880

Post-PrintAccepted author manuscript, 830 KBLicence: Unspecified

Cite this

@article{8cabfd789c3342edad2aec430f583109,

title = "An SMT solver for non-linear real arithmetic inside maple",

abstract = "We report on work-in-progress to create an SMT-solver inside Maple for non-linear real arithmetic (NRA). We give background information on the algorithm being implemented: cylindrical algebraic coverings as a theory solver in the lazy SMT paradigm. We then present some new work on the identification of minimal conflicting cores from the coverings.",

keywords = "Computer Algebra, Symbolic computation, satisfiability modulo theories, cylindrical algebraic coverings, Set covering problem",

author = "AmirHosein Sadeghimanesh and Matthew England",

note = "{\textcopyright} ACM, 2022. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Communications in Computer Algebra, vol. 56, no. 2, pp. 76-79.http://doi.acm.org/10.1145/3572867.3572880",

year = "2022",

month = nov,

day = "23",

doi = "10.1145/3572867.3572880",

language = "English",

volume = "56",

pages = "76--79",

journal = "ACM Communications in Computer Algebra",

issn = "1932-2232",

publisher = "Association for Computing Machinery (ACM)",

number = "2",

}

TY - JOUR

T1 - An SMT solver for non-linear real arithmetic inside maple

AU - Sadeghimanesh, AmirHosein

AU - England, Matthew

N1 - © ACM, 2022. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Communications in Computer Algebra, vol. 56, no. 2, pp. 76-79.http://doi.acm.org/10.1145/3572867.3572880

PY - 2022/11/23

Y1 - 2022/11/23

N2 - We report on work-in-progress to create an SMT-solver inside Maple for non-linear real arithmetic (NRA). We give background information on the algorithm being implemented: cylindrical algebraic coverings as a theory solver in the lazy SMT paradigm. We then present some new work on the identification of minimal conflicting cores from the coverings.

AB - We report on work-in-progress to create an SMT-solver inside Maple for non-linear real arithmetic (NRA). We give background information on the algorithm being implemented: cylindrical algebraic coverings as a theory solver in the lazy SMT paradigm. We then present some new work on the identification of minimal conflicting cores from the coverings.

KW - Computer Algebra

KW - Symbolic computation

KW - satisfiability modulo theories

KW - cylindrical algebraic coverings

KW - Set covering problem

U2 - 10.1145/3572867.3572880

DO - 10.1145/3572867.3572880

M3 - Article

SN - 1932-2232

VL - 56

SP - 76

EP - 79

JO - ACM Communications in Computer Algebra

JF - ACM Communications in Computer Algebra

IS - 2

ER -

An SMT solver for non-linear real arithmetic inside maple

Abstract

Bibliographical note

Keywords

Access to Document

Fingerprint

Cite this