TY - JOUR
T1 - Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
AU - Ábrahám, Erika
AU - Davenport, James H.
AU - England, Matthew
AU - Kremer, Gereon
N1 - Funding Information:
The work was not funded directly by the SC 2 project [32] but the authors were brought together by it. Matthew England was supported by EPSRC Project EP/T015748/1 (Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition).
Publisher Copyright:
© 2020 The Authors
Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
PY - 2021/2/28
Y1 - 2021/2/28
N2 - We present a new algorithm for determining the satisfiability of conjunctions of non-linear polynomial constraints over the reals, which can be used as a theory solver for satisfiability modulo theory (SMT) solving for non-linear real arithmetic. The algorithm is a variant of Cylindrical Algebraic Decomposition (CAD) adapted for satisfiability, where solution candidates (sample points) are constructed incrementally, either until a satisfying sample is found or sufficient samples have been sampled to conclude unsatisfiability. The choice of samples is guided by the input constraints and previous conflicts. The key idea behind our new approach is to start with a partial sample; demonstrate that it cannot be extended to a full sample; and from the reasons for that rule out a larger space around the partial sample, which build up incrementally into a cylindrical algebraic covering of the space. There are similarities with the incremental variant of CAD, the NLSAT method of Jovanović and de Moura, and the NuCAD algorithm of Brown; but we present worked examples and experimental results on a preliminary implementation to demonstrate the differences to these, and the benefits of the new approach.
AB - We present a new algorithm for determining the satisfiability of conjunctions of non-linear polynomial constraints over the reals, which can be used as a theory solver for satisfiability modulo theory (SMT) solving for non-linear real arithmetic. The algorithm is a variant of Cylindrical Algebraic Decomposition (CAD) adapted for satisfiability, where solution candidates (sample points) are constructed incrementally, either until a satisfying sample is found or sufficient samples have been sampled to conclude unsatisfiability. The choice of samples is guided by the input constraints and previous conflicts. The key idea behind our new approach is to start with a partial sample; demonstrate that it cannot be extended to a full sample; and from the reasons for that rule out a larger space around the partial sample, which build up incrementally into a cylindrical algebraic covering of the space. There are similarities with the incremental variant of CAD, the NLSAT method of Jovanović and de Moura, and the NuCAD algorithm of Brown; but we present worked examples and experimental results on a preliminary implementation to demonstrate the differences to these, and the benefits of the new approach.
KW - Cylindrical algebraic decomposition
KW - Non-linear real arithmetic
KW - Real polynomial systems
KW - Satisfiability modulo theories
UR - http://www.scopus.com/inward/record.url?scp=85098799338&partnerID=8YFLogxK
U2 - 10.1016/j.jlamp.2020.100633
DO - 10.1016/j.jlamp.2020.100633
M3 - Article
AN - SCOPUS:85098799338
VL - 119
JO - Journal of Logical and Algebraic Methods in Programming
JF - Journal of Logical and Algebraic Methods in Programming
SN - 2352-2208
M1 - 100633
ER -