I posted an updated version of my paper with faster timings and better text.

Abstract: “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. ”

Paper on arXiv: https://arxiv.org/abs/2004.07058

Source code: https://gitlab.com/cxxl/smtcut

Abstract: “I am presenting a novel way to use SMT (Satisfiability Modulo Theory) to compute the tropical prevariety (resp. equilibrium) of a polynomial system. 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 25 or more. Furthermore, the new approach offers a way to compute at least parts of the solution if the polyhedral approach is infeasible.”

The paper is available on arXiv: https://arxiv.org/abs/2004.07058

The source code is available at https://gitlab.com/cxxl/smtcut.

## Programming & Computer Algebra