Avoiding Larger Conflict Regions in CDCL-Style Methods for Solving SMT-NRA
摘要
A key step in CDCL-style search methods for Satisfiability Modulo the Theory of Nonlinear Real Arithmetic (SMT-NRA for short) is, given an unsat sample point, to find a conflict cell/region containing the point expressed by constructed lemmas. A larger conflict region typically reduces both backtracking frequency and computational time. Conventional techniques for constructing conflict regions are based on cylindrical algebraic decomposition (CAD), and have led to the development of single-cell projection operators [3, 7, 10]. In this paper, we propose a novel conflict region construction method that adaptively utilizes any existing single-cell projection operator. At each projection step, our approach may (i) remove more unnecessary algebraic operations (including resultant and discriminant computations) and (ii) detect more adjacent cells and merge them into a larger region. Case studies demonstrate that the new method produces larger conflict regions than conventional techniques.