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$个变量的多项式公式,公式中多项式的零级集将实数空间分解成有限的组件(单元格),并且每个多项式在每个单元格中都有恒定的符号。我们算法的关键是一种基于实根分离的新操作,称为单元格跳跃,它在沿着给定方向更新当前赋值的情况下对赋值进行“跳跃”,以便赋值可以从一个单元格跳跃到另一个单元格。一个单元环节可以调整多个变量的值,而传统的局部搜索操作(如SAT中的翻转和SMT(LIA)中的关键移动)仅改变一个变量的值。我们还设计了一个两级操作选择,以平衡成功率和效率。此外,我们的算法可以轻松推广到更广泛的SMT(NRA)子类,其中允许多项式方程相对于某些变量是线性的。实验表明,该算法在与最新的SMT求解器竞争时表现优异,并且在具有高次多项式的公式中表现特别好。