论文标题
具有满意度模型理论（SMT）求解器的计算热带流行器
Computing Tropical Prevarieties with Satisfiability Modulo Theories (SMT) Solvers
论文作者
论文摘要
提出了一种新型的使用SMT（满意度模量理论）求解器来计算多项式系统的热带预防（分别平衡）。新方法是针对使用纯粹使用多面体方法的幼稚方法进行基准测试的。事实证明，对于模型的多面体方法，SMT方法的速度要快，否则该方法将需要超过一分钟的时间来计算60倍以上，而在最坏的情况下，只有两倍的速度较慢。此外，新方法是任何时间算法，因此在多面体方法不可行时提供了一种计算溶液部分的方法。
A novel way to use SMT (Satisfiability Modulo Theories) solvers to compute the tropical prevariety (resp. equilibrium) of a polynomial system is presented. The new method is benchmarked against a naive approach that uses purely polyhedral methods. It turns out that the SMT approach is faster than the polyhedral approach for models that would otherwise take more than one minute to compute, in many cases by a factor of 60 or more, and in the worst case is only slower by a factor of two. Furthermore, the new approach is an anytime algorithm, thus offering a way to compute parts of the solution when the polyhedral approach is infeasible.
