clauseSMT: A NLSAT-Based Clause-Level Framework for Satisfiability Modulo Nonlinear Real Arithmetic Theory

本文介绍了模型构建可满足性演算（MCSAT）框架在不同算术理论的SMT问题中的应用。NLSAT是一种使用圆柱代数分解进行解释的实现，尤其在非线性实数算术约束中具有竞争力。然而，当前的冲突驱动子句学习（CDCL）算法仅考虑文字信息进行决策，因此忽略了子句级别对算术变量的影响。因此，NLSAT遇到了由于不当文字决策而引起的不必要冲突。 在本文中，我们分析了由文字决策引起的冲突，并引入了对算术变量具有直接影响的子句级别信息。我们提出了两个主要算法改进：基于子句级可行集的前瞻机制和基于算术传播的分支启发式算法。我们在我们的动态变量排序框架上实现了我们的求解器clauseSMT。实验表明，clauseSMT在非线性实数理论上与现有的SMT求解器（cvc5、Z3、Yices2）具有竞争力，并且在SMT-LIB中的可满足实例上优于所有这些求解器。我们还研究了我们提出的方法的有效性。

本论文旨在解决基于CDCL算法的SMT求解器在处理非线性实数算术约束时存在的问题，即忽略了子句级别的信息对算术变量的影响，导致不必要的冲突。

本文提出了两种算法改进方案：基于子句级可行集的前瞻机制和基于算术传播的分支启发式算法。这些改进使得求解器在SMT(QF_NRA)可满足实例上表现更好，且在非线性实数算术理论上与现有SMT求解器（cvc5、Z3、Yices2）相媲美。

本文提出的clauseSMT求解器在非线性实数算术理论上表现优异，实验结果显示其在SMT(QF_NRA)可满足实例上表现最佳。此外，本文的算法改进方案可以提高求解器的效率。本文代码已开源。

与本文相关的研究包括基于CDCL算法的SMT求解器的改进，以及非线性实数算术理论的求解器。其中一些相关论文包括：《Improving Conflict-driven Clause Learning with Non-chronological Backtracking》、《A DPLL(T) Theory Solver for Non-linear Real Arithmetic》等。