Abstract
Tropical geometry can be used to find the order of time scales of variables in chemical reaction networks and search for model reductions [SGF+15]. In this report, we consider the problem of solving tropical equilibration problems in ODE systems of the BioModels model repository. We are interested in the existence of solutions both in R and Z. We present three methods and study their scalability to solve complete equilibration problems. The first two methods, a naive polyhedral method using PtCut [Lüd20c], and a Satisfiability Modulo Theories (SMT) method recently introduced in [Lüd20a] using the SMT solver CVC4 [BCD+11], compute the set of solutions over real numbers. The SMT approach is significantly faster than the polyhedral approach, by up to two orders of magnitude. Furthermore, this method provides an anytime algorithm, thus offering a way to compute parts of the solution when the polyhedral approach is infeasible. The third method, the Constraint Programming (CP) method presented in [SFR14] and implemented in Biocham-4, computes integer equilibrations. The CP approach presents similar performance as the SMT method, mostly below two minutes computation time for the polynomial and rational fractional ODE systems in this benchmark. This method also reveals that 30% of the models that can be equilibrated over the reals have in fact no integer solution. These evaluation results show the scalability of the SMT and CP solvers for solving both real and integer tropical equilibration problems on real-size problems.