利用浮点计算辅助精确线性算术判定过程
On using floating-point computations to help an exact linear arithmetic decision procedure
AI总结：
提出一种可选的预处理阶段，通过浮点计算加速基于单纯形法的SMT求解器，保持正确性和完备性，实验表明该方法能显著提升效率。
摘要：
我们考虑无量词公式的判定问题，其原子是在实数或有理数上解释的线性不等式。该问题可使用可满足性模理论（SMT）解决，结合SAT求解器和基于单纯形的合取判定过程。最先进的SMT求解器使用有理数上的单纯形实现，对于模型检验和程序分析中出现的典型问题（稀疏不等式、小系数）表现良好，但对于其他应用（更密集的问题、更大系数）则较慢。我们提出一个简单的预处理阶段，可适配到现有SMT求解器，并可选择性地触发。尽管使用了浮点计算，我们的方法是正确且完备的——它仅影响效率。我们实现了该方法并提供了基准测试，表明这一改变使得一个朴素且缓慢的判定过程（有理数上的“教科书单纯形”）在模型检验测试用例上达到最新SMT求解器的效率，并在密集示例上明显快于最新SMT求解器。
英文摘要：
We consider the decision problem for quantifier-free formulas whose atoms are linear inequalities interpreted over the reals or rationals. This problem may be decided using satisfiability modulo theory (SMT), using a mixture of a SAT solver and a simplex-based decision procedure for conjunctions. State-of-the-art SMT solvers use simplex implementations over rational numbers, which perform well for typical problems arising from model-checking and program analysis (sparse inequalities, small coefficients) but are slow for other applications (denser problems, larger coefficients). We propose a simple preprocessing phase that can be adapted on existing SMT solvers and that may be optionally triggered. Despite using floating-point computations, our method is sound and complete - it merely affects efficiency. We implemented the method and provide benchmarks showing that this change brings a naive and slow decision procedure ("textbook simplex" with rational numbers) up to the efficiency of recent SMT solvers, over test cases arising from model-checking, and makes it definitely faster than state-of-the-art SMT solvers on dense examples.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
