This page describes a series of tests we did on the rewrite systems with
the single rules a(b(x)) -> b(a(x)), a(b(x)) -> b(b(a(x))), and
a(b(x)) -> b(b(b(a(x)))), respectively. We measured the used time for
various configurations of cdiprover3 until the answer "YES" or "MAYBE" was
given, and counted the number of propositional variables in the formula
given to MiniSAT.
The following color code is used in the tables below:
| YES, we have termination and exponential/quadratic derivational complexity |
| MAYBE, no proof found |
| A TIMEOUT has occurred |
| An error has occurred |
The tests were run single-threaded on a server equipped with 8 AMD Opteron 2.8 GHz dual core
processors with 64GB of RAM. All times are given in seconds. For all tests, a timeout of 60
seconds was used. We did not use the incremental search strategy in these tests ("-i" flag not
set).
Results for a(b(x)) -> b(a(x))
|
Delta-restricted interpretations |
Delta-linear interpretations |
| bits |
propositional variables |
time |
propositional variables |
time |
| 1 |
54 |
0.013 |
54 |
0.013 |
| 2 |
396 |
0.049 |
846 |
0.100 |
| 3 |
944 |
0.121 |
2271 |
0.363 |
| 4 |
1684 |
0.226 |
4220 |
0.622 |
| 5 |
2632 |
0.371 |
6750 |
1.139 |
Results for a(b(x)) -> b(b(a(x)))
|
Delta-restricted interpretations |
Delta-linear interpretations |
| bits |
propositional variables |
time |
propositional variables |
time |
| 1 |
315 |
0.045 |
315 |
0.045 |
| 2 |
2426 |
0.651 |
6408 |
1.170 |
| 3 |
5935 |
3.266 |
18416 |
3.066 |
| 4 |
10602 |
7.262 |
34976 |
6.404 |
| 5 |
16553 |
27.350 |
55317 |
13.214 |
Results for a(b(x)) -> b(b(b(a(x))))
For this TRS, the resulting formula is too big to make counting its variables
feasible.
|
Delta-restricted interpretations |
Delta-linear interpretations |
| bits |
variable occurrences |
time |
variable occurrences |
time |
| 1 |
|
0.268 |
|
0.283 |
| 2 |
|
2.816 |
|
8.409 |
| 3 |
|
15.693 |
|
40.103 |
| 4 |
|
57.800 |
|
33.833 |
| 5 |
|
48.802 |
|
43.370 |