Empirical Evaluation of "Search Techniques for Rational Polynomial Orders"

Polynomial interpretations are a standard technique used in almost all tools for proving termination of term rewrite systems (TRSs) automatically. Traditionally, one uses interpretations with polynomials over the naturals. But recently, it was shown that interpretations with polynomials over the rationals can be significantly more powerful. However, searching for such interpretations is considerably more difficult than for natural polynomials. Moreover, while there exist highly efficient SAT-based techniques for finding natural polynomials, no such techniques had been developed for rational polynomials yet.

In the paper Search Techniques for Rational Polynomial Orders, we solve the two main problems when applying rational polynomial interpretations in practice:

  1. We develop new criteria to decide when to use rational instead of natural polynomial interpretations.
  2. Afterwards, we present SAT-based methods for finding rational polynomial interpretations and evaluate them empirically.

Implementation in AProVE

We have integrated our approach into the automated termination prover AProVE. To experiment with this new version of AProVE, please use the special web interface.

Examples

In our experiments below, we want to assess the power of our contributions. Therefore, we tested the new version of AProVE on all 2061 term and string rewrite systems from the Termination Problem Data Base (TPDB) 4.0. This is the collection of problems used in the annual International Termination Competition 2007. We compared the performance of our new version of AProVE against the version of AProVE that won the termination competition for term rewrite systems in 2007.

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:

Results and Discussion

In the following table, we only used the dependency graph and reduction pair processor, but no other termination techniques. In this way, one can best measure the effect of rational versus natural polynomial orders, both in terms of power and of runtimes. In the first technique Nat, we only searched for natural polynomials where the coefficients take values from {0,1,2,3,4}. In the technique Rat + Sect. 4.1, we used rational coefficients from {p/4 | 0 ≤ p ≤ 16} instead and applied the transformational technique of Sect. 4.1 to convert constraints over the rationals to constraints over the naturals. Here, we always search for rational polynomials, whereas in the technique Rat + Sect. 4.1 + Sect. 3 we only search for rationals if this is suggested by our criteria from Sect. 3. Otherwise, we use natural polynomials with coefficients from {0,1,2,3,4}. Finally, in the technique Rat + Sect. 4.2 we (always) use rational coefficients from { 2-2, 2-1, 20, 21, 22, 0} and apply the direct SAT-encoding from Sect. 4.2. We also experimented with different ranges for the coefficients, but the above ranges gave the best results as far as power and runtimes are concerned.

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.

SettingYesSucTimeFulTime
Nat6061.92.9Full Table
Rat + Sect. 4.17423.115.4Full Table
Rat + Sect. 4.1 + Sect. 36852.611.0Full Table
Rat + Sect. 4.26966.129.2Full 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 [17] for generating rational interpretations, implemented in MU-TERM. More precisely, we compare this version (MU-TERM + [17]) with a version of MU-TERM where instead of [17] 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 [17].

SettingYesFulTime
MU-TERM + [17]6210.1Full Table
MU-TERM + Rat + Sect. 4.1654.1Full 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.

SettingYesNoSucTimeFulTime
AProVE 0710892383.829.6Full Table
AProVE-Rat-Full11192385.230.4Full Table
AProVE-Rat11182384.930.1Full 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.