一句话：通过子句级前瞻与算术传播分支启发式，使 NLSAT 在非线性实数算术上更具竞争力。
NLSAT 是基于 MCSAT 框架、以柱形代数分解（CAD）作解释的非线性实数算术（NRA）SMT 求解器。但现有 CDCL 风格算法在决策时只考虑文字信息，忽略子句对算术变量的影响，易因文字选择次优而产生不必要的冲突。本文分析文字决策引发的冲突，将直接影响算术变量的子句级信息纳入求解过程，提出两项改进：基于子句级可行集的前瞻机制与基于算术传播的分支启发式，并在动态变量排序框架上实现求解器 clauseSMT。实验显示，clauseSMT 在 NRA 问题上与 CVC5、Z3、YICES2 具有竞争力，在 SMT-LIB 的 QF_NRA 可满足实例上优于全部对比求解器，作者还评估了所提方法的有效性。
The Model-Constructing Satisfiability Calculus (MCSAT) framework has been applied to SMT problems over various arithmetic theories. NLSAT, an implementation using cylindrical algebraic decomposition (CAD) for explanation, is especially competitive for nonlinear real arithmetic (NRA) constraints. However, current Conflict-Driven Clause Learning (CDCL)-style algorithms only consider literal information when making decisions, and thus ignore the influence of clauses on arithmetic variables. This limitation may lead NLSAT to encounter unnecessary conflicts due to suboptimal literal choices. To address this issue, we analyze conflicts caused by literal decisions and incorporate clause-level information that directly affects arithmetic variables. We propose two main algorithmic improvements: a clause-level feasible-set-based look-ahead mechanism and an arithmetic propagation-based branching heuristic. We implement our solver, named clauseSMT, based on a dynamic variable ordering framework. Experiments indicate that clauseSMT is competitive on nonlinear real arithmetic problems compared with existing SMT solvers (CVC5, Z3, YICES2), and it outperforms all of them on satisfiable instances of SMT(QF_NRA) in SMT-LIB. We also evaluate the effectiveness of our proposed methods.
DOI 原文 ·
@inproceedings{paperbot9552,
title = {Improving NLSAT for Nonlinear Real Arithmetic},
author = {Zhonghan Wang},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00128}
}