Name
Title | ||
|---|---|---|
Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings |
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1016/j.jlamp.2020.100633 | Journal of Logical and Algebraic Methods in Programming |
Keywords | DocType | Volume |
Satisfiability modulo theories,Non-linear real arithmetic,Cylindrical algebraic decomposition,Real polynomial systems | Journal | 119 |
ISSN | Citations | PageRank |
2352-2208 | 0 | 0.34 |
References | Authors | |
0 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Erika Ábrahám | 1 | 830 | 63.17 |
| J. H. Davenport | 2 | 109 | 21.82 |
| England Matthew | 3 | 0 | 0.34 |
| Gereon Kremer | 4 | 3 | 1.76 |