Empirical Evaluation of "Proving Termination using Recursive Path Orders and SAT Solving"

In the paper Proving Termination using Recursive Path Orders and SAT Solving we present a novel encoding from recursive path order (RPO) with argument filters to propositional logic. This extends the results of Solving Partial Order Constraints for LPO Termination and SAT Solving for Argument Filterings from path orders with left-to-right lexicographic comparisons (LPO) to recursive path orders (RPO) where a status function denotes if arguments are compared lexicographically w.r.t. a permutation or as multisets. The paper presents both an encoding for direct application of RPO and an encoding for application in the context of the popular DP Framework which allows the use of argument filters. In our experiments, we want to assess the power of our new SAT-based implementation of RPO for both direct analysis and for analysis with argument filters. Therefore, we compare our implementation to the existing non-SAT-based implementation in the termination analyzer AProVE.

Implementation in AProVE

We integrated our approach in the termination tool AProVE which implements the DP framework. A special version of AProVE that allows to repeat the experiments below can be accessed via a special web interface.

Examples

In our experiments, we tested the new SAT-based and the old non-SAT-based implementation on the examples of the Termination Problem Data Base (TPDB). This is the collection of problems used in the International Termination Competition. It contains 865 TRSs from different sources as a benchmark for termination analysis of term rewriting.

Experiments

The experiments were run on a 2.2 GHz AMD Athlon 64 with a time-out of 60 seconds (as in the International Termination Competition). For each encoding we give the number of TRSs which could be proved terminating (with the number of time-outs in brackets) and the analysis time (in seconds) for the full collection. The first table compares our new SAT-based approach for direct application of path orders to the previous dedicated solvers for path orders in AProVE 1.2 which did not use SAT solving. The columns contain the data for LPO with strict and non-strict precedence (denoted lpo/qlpo), for LPO with status (lpos/qlpos), for MPO (mpo/qmpo), and for RPO with status (rpo/qrpo). Click on the column headers to view a detailed table with the individual results of the column. Click on "[Details]" to the right of a row to view a detailed table with the individual results of the row.

Solver lpo qlpo lpos qlpos mpo qmpo rpo qrpo
(direct) YesTOTimeYesTOTimeYesTOTimeYesTOTimeYesTOTimeYesTOTimeYesTOTimeYesTOTime
SAT-based123 031.0127 044.7141 026.1155 040.6 92 049.4 98 074.2146 050.0162 085.3[Details]
dedicated123 5334.4127161426.3141 6460.4154453291.7 92 7653.2 98312669.114510908.6158654708.2[Details]

The table above shows that with our new SAT encoding, performance improves by orders of magnitude over existing solvers for direct analysis with path orders. Note that the SAT-based solvers always provide an answer well within the time limit while there are many time-outs (especially for path orders based on non-strict precedences) for the dedicated solvers.

The following table compares our new SAT-based approach for RPO with argument filters to the previous dedicated solvers for path orders and argument filters in AProVE 1.2.
The techniques used for simplifying DP problems (P,R) in the DP framework are called DP processors. Apart from the processor based on reduction pairs mentioned in Section 4 of the paper (deleting strict rules from P), for the analysis within the DP framework we also used a processor based on the dependency graph, which is the other main processor of the DP framework. This processor is used to split up dependency pair problems into smaller ones.

Solver lpo qlpo lpos qlpos mpo qmpo rpo qrpo
(arg. filt.) YesTOTimeYesTOTimeYesTOTimeYesTOTimeYesTOTimeYesTOTimeYesTOTimeYesTOTime
SAT-based357 079.3389 0199.6362 069.0395 2261.1369 0110.9408 1 267.8375 0108.8416 2331.4[Details]
dedicated350554039.6374795469.4355574522.8380926476.5359695169.7391825839.5364745536.63941027186.1[Details]

The table shows that with our new SAT encoding, performance again improves by orders of magnitude over existing solvers. Here, the increase of efficiency is even more pronounced and there are many more time-outs for the dedicated solvers. Note that without a time-out, this effect would be aggravated further.