Encoding DP Techniques and Control Strategies
for Maximal Completion

General

This site provides supporting material for the paper Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion by Haruhiko Sato and Sarah Winkler.

This paper describes two advancements of SAT-based Knuth- Bendix completion as implemented in Maxcomp. (1) Termination techniques using the dependency pair framework are encoded as satisfiability problems, including dependency graph and reduction pair processors. (2) Instead of relying on pure maximal completion, diㄦent SAT-encoded control strategies are exploited. Experiments show that these developments let Maxcomp improve over other automatic completion tools, and produce novel complete systems.

Download

You may want to download the sources and a 64bit executable.

Usage

The usage of MaxcompDP is as follows:
$ ./maxcompdp -M auto eq_systems/slothrop_cge.trs
The option -M allows to specify a strategy for MaxcompDP. Options include auto, lpo, kbo, mpol, dp, dg, dgk, maxcomp, red, cpred, and comp. The options -N and -K allow to set the n and k parameters. The input file is supposed to be in the trs format.

Experiments

The following tables summarize results for the test bed comprising 115 equational systems from the distribution of mkbTT, run on a system equipped with an Intel Core i7 with four cores of 2.1GHz each and 7.5 GB of memory. Each ES was given a time limit of 600 seconds,
  1. comparison with other tools
    comparison with other automatic completion tools: the original version of Maxcomp, mkbTT, and KBCV.
  2. termination strategies
    comparison of LPO, DP, DG, DG-2SCC (using Cred+comp+cpred), and the auto setting
  3. control strategies for DP techniques
    comparison of Smaxcomp, Sunoriented, Sred, Scomp, Scpred and Sred+comp+cpred, using DP([LPol,LPO])
  4. control strategies for LPO
    comparison of Cmaxcomp and Cred+comp+cpred, using LPO
  5. k values
    comparison of a) fixing k=2 and b) initially choosing k=6 for two iterations
  6. completions of CGE6 and CGE7

k=2k=6 or 2
0.01 0.00
0.07 0.05
0.01 0.01
0.01 0.01
0.01 0.00
17.98 10.89
18.03 15.69
16.94 18.38
45.71 46.55
0.73 1.30
0.74 0.99
1.45 2.71
2.76 3.49
0.01 0.01
4.62 2.19
5.28 2.38
0.00 0.00
45.05
155.31 104.41
0.30 0.14
151.62
0.03 0.01
0.64 0.02
36.19
1.73 0.50
0.00 0.00
3.83 2.04
2.51 1.36
22.06
5.20 2.16
5.10 3.67
0.03 0.01
0.01 0.01
0.04 0.02
0.02 0.05
0.16 0.02
0.42 0.32
0.01 0.01
0.02 0.01
0.04 0.02
0.06 0.03
0.04 0.06
0.18 0.32
10.96 19.63
0.03 0.03
0.01 0.01
0.01 0.00
5.74 6.99
76.92 4.56
0.08 0.16
0.02 0.02
0.00 0.00
0.01 0.01
0.01 0.00
6.23 5.68
1.31 1.40
2.48 1.28
0.01 0.01
0.00 0.00
0.00 0.01
0.01 0.03
0.00 0.01
2.06 0.92
1.32 0.68
0.11 0.09
0.00 0.00
0.46 0.31
17.54 7.41
32.24 15.59
17.21 120.03
14.61 42.91
30.70 12.29
131.82
290.15 25.58
37.99 20.30
34.46 103.66
86.91
0.03 0.00
0.03 0.00
0.01 0.01
4.75 3.61
0.00 0.01
0.01 0.01
0.01 0.01
1.18 1.41
1.03 0.54
2.84 1.39
0.00 0.00
8.44 4.14
15.34 24.44
2.31 1.46
2.81 1.49
2.63 1.50
0.01 0.01
1.17 0.76
0.05 0.03
0.00 0.00
successes 9197
avg. time 10.05911.587