In the paper Search Techniques for Rational Polynomial Orders, we solve the two main problems when applying rational polynomial interpretations in practice:
For our experiments, the tools were run on Dual Intel Xeons at 2.33 GHz. For each example, we imposed a time limit of 120 seconds (corresponding to the way tools were evaluated in the termination competition 2007).
We use MiniSAT for the SAT solving. The SAT library SAT4J is used to transform general propositional formulas into CNF using Tseitin's algorithm. In principle, any SAT solver which can test satisfiability of CNFs given in DIMACS format can be used by AProVE.
The examples from the paper can be experimented with by clicking on one of the six buttons below:
The column Yes shows the number of TRSs where the termination proof succeeds. SucTime gives the average runtime for successful examples and FulTime gives the average runtime for all examples. Clicking on "Full Table" gives the full table with detailed proof output of the respective tools. The full table also allows to load an individual example into our web interface.
|Rat + Sect. 4.1||742||3.1||15.4||Full Table|
|Rat + Sect. 4.1 + Sect. 3||685||2.6||11.0||Full Table|
|Rat + Sect. 4.2||696||6.1||29.2||Full Table|
Comparing Nat with the other settings shows that rational polynomials can significantly increase power, but they also increase runtimes. The comparison of Rat + Sect. 4.1 with Rat + Sect. 4.1 + Sect. 3 shows the usefulness of our criteria from Sect. 3: if one applies these criteria, then runtimes are not increased that much anymore, but (as long as one does not use any other termination techniques) one also loses several examples where rational interpretations were needed. Finally, the comparison with the last setting in the table shows that the method of Sect. 4.1 which transforms constraints over the rationals to constraints over the naturals is preferable to the direct SAT encoding from Sect. 4.2.
The next experiment compares Rat + Sect. 4.1 with the existing constraint-based method  for generating rational interpretations, implemented in MU-TERM. More precisely, we compare this version (MU-TERM + ) with a version of MU-TERM where instead of  one calls AProVE (with the technique of Rat + Sect. 4.1) externally. Since MU-TERM generates the polynomial constraints and it only calls AProVE with this set of constraints, the implementation of the criteria from Sect. 3 cannot be used here. In this table, we only ran MU-TERM on a collection of 79 TRSs from the TPDB. These are TRSs where MU-TERM needs rational polynomials in order to succeed with the proof. It turns out that in spite of the external calls, the new SAT-based implementation is indeed significantly faster than the previous non-SAT-based method of .
|MU-TERM + ||62||10.1||Full Table|
|MU-TERM + Rat + Sect. 4.1||65||4.1||Full Table|
Finally, to measure the usefulness of our contributions in full termination provers, the next table compares the performance of full versions of AProVE on all 2061 examples. Here, many termination techniques are used in addition to the dependency graph and reduction pair processor. Moreover, there are also techniques to disprove termination (cf. column No). This is a more realistic setting than in the first table, because in reality, polynomial interpretations are just one of many methods applied in termination tools.
|AProVE 07||1089||238||3.8||29.6||Full Table|
The above table shows that the results of the current paper are also useful when integrating them into such a powerful prover. AProVE-07 is the version which participated in the Termination Competition 2007 (and which won this competition in the category of TRSs). AProVE-Rat-Full differs from AProVE-07 by using rational polynomials with the setting Rat + Sect. 4.1 and AProVE-Rat uses Rat + Sect. 4.1 + Sect. 3 instead. It is interesting to note that when integrating rational polynomials into this full version of AProVE, the criteria of Sect. 3 have very positive effects. In other words, they reduce the runtimes and hardly affect the power.