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

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

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.

Setting | Yes | SucTime | FulTime | |
---|---|---|---|---|

Nat | 606 | 1.9 | 2.9 | Full Table |

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 [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].

Setting | Yes | FulTime | |
---|---|---|---|

MU-TERM + [17] | 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.

Setting | Yes | No | SucTime | FulTime | |
---|---|---|---|---|---|

AProVE 07 | 1089 | 238 | 3.8 | 29.6 | Full Table |

AProVE-Rat-Full | 1119 | 238 | 5.2 | 30.4 | Full Table |

AProVE-Rat | 1118 | 238 | 4.9 | 30.1 | 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.