Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
Journal of Logical and Algebraic Methods in Programming(2021)
摘要
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.
更多查看译文
关键词
Satisfiability modulo theories,Non-linear real arithmetic,Cylindrical algebraic decomposition,Real polynomial systems
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络