Empirical Evaluation of "SAT Solving for Termination Analysis with Polynomial Interpretations"

Finding a solution for Diophantine constraints is in general undecidable. Even if one restricts the variables in these constraints to a finite domain (e.g., all naturals less than 4), the problem is still NP-complete. Therefore, the search for such interpretations is a main bottleneck in most termination provers. In the paper SAT Solving for Termination Analysis with Polynomial Interpretations we present a novel encoding of this NP-complete problem to the satisfiability problem of propositional formulas. By applying modern SAT solvers we obtain speedups in orders of magnitude compared to dedicated search algorithms.

In our experiments, we want to assess the power and efficiency of our new SAT-based back-ends. Therefore, we compare them to existing non-SAT-based back-ends.

Implementation in AProVE

Tools

• AProVE-SAT 2.0-prealpha3:
  The Diophantine inequality constraints are transformed into propositional SAT problems as described in the paper. We use either MiniSAT or SAT4J for the SAT solving. The latter is always 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.
• AProVE-PB 2.0-prealpha3:
  The Diophantine inequality constraints are transformed into pseudo-Boolean constraints and then linearized using Fortet's linearization scheme. The linear PB constraints are solved by either the Pueblo PB-SAT solver or by MiniSAT+.
• AProVE 1.2:
  The Diophantine inequality constraints are solved by a state-of-the-art finite domain constraint solver. This is based on the specialized finite domain constraint satisfaction procedure of Contejean et al. For negative polynomial interpretations, a specialized trial-and-error search is performed.
• AProVE-CiME 2.0-prealpha3:
  The Diophantine inequality constraints are solved by the popular Diophantine solver of the CiME tool. This solver is also based on the Contejean algorithm for finite domain constraint solving.
• AProVE-CLP 2.0-prealpha3:
  The Diophantine inequality constraints are transformed into a constraint logic program. This is then handled by the CLP(fd) engine of SICStus Prolog.
• TTT:
  The Tyrolean Termination Tool is a powerful and very efficient termination analyzer. Its implementation of Diophantine constraint solving is based on a generate-and-test algorithm.

Examples and Settings

We configured all tools to use a basic version of the DP method, where in addition to polynomial interpretations, the tools also apply the dependency graph refinement to split up sets of dependency pairs. Moreover, do not build constraints for all rules, but just for those that are "usable". For more information on these enhancements of the DP method, the reader is referred to The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. Thus, in total the strategy applied by all tools is:

1. Compute the dependency pairs from the TRS.
2. Estimate the dependency graph.
3. For each maximal strongly connected component (SCC) of the graph:
   • Generate constraints for the dependency pairs and the usable rules.
   • Generate Diophantine inequalities over naturals.
   • Call a solver to find a solution for the constraints.
   • If there is a solution, delete the strict dependency pairs and continue with 2.

For our experiments, the tools were run on an AMD Athlon 64 at 2.2 GHz. For each example, we imposed a time limit of 60 seconds (corresponding to the way tools are evaluated in the annual competition) or of 10 minutes, indicated by the "Limit" column in the following tables.

Experiments

			AProVE-SAT (MiniSAT)			AProVE-SAT (SAT4J)			AProVE-PB (Pueblo)			AProVE-PB (MiniSAT+)
Limit	Range	Degree	Yes	TO	Time	Yes	TO	Time	Yes	TO	Time	Yes	TO	Time
60s	1	1	421	0	45.5	421	0	27.4	421	0	61.6	421	0	55.4	[Details]
60s	2	1	431	0	91.8	431	0	89.8	431	0	158.5	431	1	170.5	[Details]
60s	3	1	434	0	118.6	434	0	158.6	434	1	222.1	434	2	237.5	[Details]
60s	3	sm	440	51	5585.9	414	124	10344.4	427	82	7280.3	434	82	7254.5	[Details]
10m	1	1	421	0	45.5	421	0	27.4	421	0	61.6	421	0	55.4	[Details]
10m	2	1	431	0	91.8	431	0	89.8	431	0	158.5	431	1	710.5	[Details]
10m	3	1	434	0	118.6	434	0	158.6	434	0	689.6	434	1	817.5	[Details]
			AProVE 1.2			AProVE-CLP			AProVE-CiME			TTT
Limit	Range	Degree	Yes	TO	Time	Yes	TO	Time	Yes	TO	Time	Yes	TO	Time
60s	1	1	421	1	151.8	420	16	1357.8	408	1	168.3	326	32	2568.5	[Details]
60s	2	1	414	48	3633.2	420	37	3558.3	408	43	3201.0	335	83	5677.6	[Details]
60s	3	1	408	81	5793.2	407	91	6459.5	402	67	5324.1	338	110	7426.9	[Details]
60s	3	sm	404	171	11608.1	367	145	10357.4	361	147	10107.7	n/a	n/a	n/a	[Details]
10m	1	1	421	1	691.8	421	11	7852.2	408	0	332.7	328	16	14007.8	[Details]
10m	2	1	418	41	27888.4	423	25	18795.6	412	33	22190.4	337	68	45046.6	[Details]
10m	3	1	415	53	38286.4	420	51	41493.8	407	46	33873.6	340	91	61209.2	[Details]
			For details on individual examples and runtimes please click on [Details] in the right-most column.

The comparison of the SAT-based configurations AProVE-SAT and AProVE-PB with the non-SAT-based configurations shows that the provers based on SAT solving with our proposed encoding are faster by orders of magnitude. This holds in particular if one considers a higher time limit or polynomials with higher coefficients or degrees (which are needed to increase the number of "Yes"-results, i.e., to increase the power of automated termination proving). Note that if "Degree" is 1, there are no time-outs in the configuration AProVE-SAT, whereas the non-SAT-based configurations have many time-outs. Due to the increased efficiency, the number of examples where termination can be proved within the time limit is considerably higher in the SAT-based configurations. Comparing the SAT-based configurations AProVE-SAT and AProVE-PB shows that the approach of converting termination problems to propositional formulas is currently preferable to the related approach of converting them to pseudo-boolean constraints.

For efficiency, our implementation uses several optimizations:

(a) Simplification: In addition to standard simplifications for Diophantine constraints and for propositional formulas, we developed a new graph-based approach to detect possible simplifications of Diophantine constraints quickly.

(b) Sharing: We use sharing for common subexpressions, both on the level of Diophantine constraints and on the level of propositional formulas.

(c) Tracking maximum values: By taking into account that Diophantine variables are only instantiated by values from a certain set (e.g., {0, ..., 2^k-1}), one can keep track of the maximum possible values for all polynomials occurring in the Diophantine constraint. This can help to improve the conversion from Diophantine constraints to tuples of propositional formulas. The reason is that we can detect cases where the most significant bits are equivalent to 0.

The next table shows the effect of our optimizations (with linear polynomials and a 60 s time limit). While the configuration AProVE-SAT uses all optimizations (a) - (c), we also give the results obtained if one omits any one of these optimizations. The table demonstrates that each optimization has a considerable positive effect, in particular if one regards higher ranges for the coefficients.

	AProVE-SAT (MiniSAT)			no optimization (a)			no optimization (b)			no optimization (c)
Range	Yes	TO	Time	Yes	TO	Time	Yes	TO	Time	Yes	TO	Time
1	421	0	45.5	421	0	56.6	421	0	49.7	421	0	50.1	[Details]
2	431	0	91.8	431	0	107.5	431	0	93.9	431	0	114.7	[Details]
3	434	0	118.6	434	1	159.4	434	0	202.8	434	0	138.7	[Details]
	For details on individual examples and runtimes please click on [Details] in the right-most column.

The last table demonstrates the use of SAT solving when handling negative polynomials with a time limit of 60 seconds. Here, if the "Range" is n, then the constant coefficient is allowed to take values from {-n, ..., n}.

	AProVE-SAT (MiniSAT)			AProVE 1.2			TTT
Range	Yes	TO	Time	Yes	TO	Time	Yes	TO	Time
1	440	0	98.0	441	22	1863.7	341	106	7307.3	[Details]
2	479	1	305.4	460	126	8918.3	360	181	12337.3	[Details]
3	483	4	1092.4	434	221	15570.9	361	247	16927.7	[Details]
	For details on individual examples and runtimes please click on [Details] in the right-most column.

Again, the SAT-based configuration is much faster and substantially more powerful than the non-SAT-based ones. Compared to the results for non-negative polynomials, a few timeouts occur for larger ranges, but negative polynomials increase the power significantly whereas the runtimes only increase moderately.

The SAT-based implementation of polynomial interpretations was used by AProVE in the International Competition of Termination Tools 2006. Here, AProVE was configured to use several other termination techniques in addition to polynomial interpretations. Due to the speed of our new SAT-based approach, AProVE could try polynomial interpretations (also with higher ranges) as one of the first termination techniques. In case of failure, there was still enough time to try other termination techniques afterwards. With a time limit of 60s for each example, AProVE could prove termination of 633 TRSs and thereby it was the winner of the competition. In this way, the contributions of this paper increase not only the efficiency, but also the power of automated termination proving.

To summarize, automated termination analysis is indeed a field where SAT solving has turned out to be extremely useful. At the same time, this field also poses new challenges for SAT solving, since for higher ranges and higher degrees of the polynomials, one sometimes obtains SAT problems which are hard for current SAT solvers (e.g., problems with less than 9000 variables but several days of runtime). We have therefore submitted some of these problems to the SAT competition 2007.