Satisfiability modulo nonlinear real arithmetic theory (SMT(NRA)) solving is essential to multiple applications, including program verification, program synthesis and software testing. In this context, recently model constructing satisfiability calculus (MCSAT) has been invented to directly search for models in the theory space. Although following papers discussed practical directions and updates on MCSAT, less attention has been paid to the detailed implementation. In this paper, we present an efficient implementation of dynamic variable orderings of MCSAT, called dnlsat. We show carefully designed data structures and promising mechanisms, such as branching heuristic, restart, and lemma management. Besides, we also give a theoretical study of potential influences brought by the dynamic variablr ordering. The experimental evaluation shows that dnlsat accelerates the solving speed and solves more satisfiable instances than other state-of-the-art SMT solvers. Demonstration Video: https://youtu.be/T2Z0gZQjnPw Code: https://github.com/yogurt-shadow/dnlsat/tree/master/code Benchmark https://zenodo.org/records/10607722/files/QF_NRA.tar.zst?download=1

翻译：非线性实数运算可满足性模理论（SMT(NRA)）求解在程序验证、程序综合与软件测试等多项应用中至关重要。在此背景下，近年来提出的模型构造可满足性演算（MCSAT）可直接在理论空间中搜索模型。尽管后续研究探讨了MCSAT的实践方向与改进，其具体实现细节却较少受到关注。本文提出一种高效的动态变量排序MCSAT实现方法，称为dnlsat。我们展示了精心设计的数据结构及分支启发式、重启机制与引理管理等有效策略。此外，本文还从理论上分析了动态变量排序可能带来的影响。实验评估表明，相较于其他前沿SMT求解器，dnlsat显著提升了求解速度并解决了更多可满足性实例。演示视频：https://youtu.be/T2Z0gZQjnPw 代码：https://github.com/yogurt-shadow/dnlsat/tree/master/code 基准测试集：https://zenodo.org/records/10607722/files/QF_NRA.tar.zst?download=1