亚热带可满足性
Subtropical Satisfiability
摘要：
无量化器非线性算法（QF_NRA）在可满足性模理论求解（SMT）的许多应用中出现。因此，SMT理论求解器中相应约束的有效推理是高度相关的。我们提出了一个新的不完整的，但有效的和终止的方法来识别可满足的实例。该方法是来自亚热带方法最近推出的符号计算的背景下，计算单个非常大的多元多项式的实零点。我们的方法需要作为输入的严格的多项式不等式，这代表了超过40%的QF_NRA节的SMT-LIB库的基准连接。该方法将多项式抽象为自然数上的指数向量，并标记相应系数的符号。然后，依次使用SMT来解决实数上的线性问题，以探索性地找到合适的点，这些点可以转换回原始问题的满意点。SMT-LIB系统的实验表明，我们的方法本身不是一个足够强大的决策过程，但一个有价值的启发式使用的技术组合。
英文摘要：
Quantifier-free nonlinear arithmetic (QF_NRA) appears in many applications of satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning for corresponding constraints in SMT theory solvers is highly relevant. We propose a new incomplete but efficient and terminating method to identify satisfiable instances. The method is derived from the subtropical method recently introduced in the context of symbolic computation for computing real zeros of single very large multivariate polynomials. Our method takes as input conjunctions of strict polynomial inequalities, which represent more than 40% of the QF_NRA section of the SMT-LIB library of benchmarks. The method takes an abstraction of polynomials as exponent vectors over the natural numbers tagged with the signs of the corresponding coefficients. It then uses, in turn, SMT to solve linear problems over the reals to heuristically find suitable points that translate back to satisfying points for the original problem. Systematic experiments on the SMT-LIB demonstrate that our method is not a sufficiently strong decision procedure by itself but a valuable heuristic to use within a portfolio of techniques.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
