Satisfiability Modulo the Theory of Nonlinear Real Arithmetic, SMT(NRA) for short, concerns the satisfiability of polynomial formulas, which are quantifier-free Boolean combinations of polynomial equations and inequalities with integer coefficients and real variables. In this paper, we propose a local search algorithm for a special subclass of SMT(NRA), where all constraints are strict inequalities. An important fact is that, given a polynomial formula with $n$ variables, the zero level set of the polynomials in the formula decomposes the $n$-dimensional real space into finitely many components (cells) and every polynomial has constant sign in each cell. The key point of our algorithm is a new operation based on real root isolation, called cell-jump, which updates the current assignment along a given direction such that the assignment can `jump' from one cell to another. One cell-jump may adjust the values of several variables while traditional local search operations, such as flip for SAT and critical move for SMT(LIA), only change that of one variable. We also design a two-level operation selection to balance the success rate and efficiency. Furthermore, our algorithm can be easily generalized to a wider subclass of SMT(NRA) where polynomial equations linear with respect to some variable are allowed. Experiments show the algorithm is competitive with state-of-the-art SMT solvers, and performs particularly well on those formulas with high-degree polynomials.

翻译：摘要：非线性实数算术理论的可满足性模理论（简称SMT(NRA)）研究多项式公式的可满足性，这类公式是由整数系数、实数变量的多项式方程与不等式构成的无量词布尔组合。本文针对SMT(NRA)的一个特殊子类（所有约束均为严格不等式）提出局部搜索算法。重要事实在于：给定含$n$个变量的多项式公式，其中多项式的零水平集将$n$维实空间分解为有限个连通分量（胞腔），且每个多项式在各胞腔内符号恒定。算法核心是基于实根分离的新操作——胞腔跳跃，该操作沿着给定方向更新当前赋值，使赋值能从当前胞腔"跳跃"至另一胞腔。单次胞腔跳跃可同时调整多个变量值，而传统局部搜索操作（如SAT中的翻转、SMT(LIA)中的关键移动）仅改变单个变量值。我们进一步设计了两级操作选择机制以平衡成功率与效率。此外，该算法可轻松推广至允许存在关于某变量线性多项式方程的SMT(NRA)子类。实验表明，该算法与现有最优SMT求解器具有竞争力，尤其擅长处理含高次多项式的公式。