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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Avoiding Larger Conflict Regions in CDCL-Style Methods for Solving SMT-NRA

  • Xinpeng Ni,
  • Tianyi Ding,
  • Bican Xia

摘要

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.