Summary of all benchmark classes in the SLparse competition
This section presents the results for the benchmark classes of the First
Answer Set Programming System Competition.
Each single run was limited to 600 seconds execution time and 448 MB RAM memory
usage.
For the sake of completeness, we provide similar data for all benchmarks used in
each competition class. In addition, the tables give the number of instances
selected from each class ("#") and provide additional information on the
satisfiable and unsatisfiable instances.
Results for SAT and UNSAT instances
| Benchmark Class | # | Solved | % | SAT | % | UNSAT | % | min | max | avg |
|---|
| RLP-200 | 5 | 89/95 | 93.68 | 18/19 | 94.74 | 71/76 | 93.42 | 0.25 | 465.69 | 60.94 |
| RLP-150 | 5 | 87/95 | 91.58 | 17/19 | 89.47 | 70/76 | 92.11 | 0.25 | 183.29 | 14.17 |
| Factoring | 4 | 69/76 | 90.79 | 36/38 | 94.74 | 33/38 | 86.84 | 0.63 | 549.80 | 64.09 |
| verify Test - variable Search Space | 5 | 81/95 | 85.26 | 81/95 | 85.26 | 0/0 | | 0.24 | 303.32 | 16.43 |
| Random Non-Tight | 5 | 75/95 | 78.95 | 41/57 | 71.93 | 34/38 | 89.47 | 0.41 | 518.08 | 123.56 |
| Knights Tour | 5 | 71/95 | 74.74 | 71/95 | 74.74 | 0/0 | | 1.04 | 248.97 | 28.29 |
| Su-Doku | 3 | 42/57 | 73.68 | 42/57 | 73.68 | 0/0 | | 18.15 | 176.69 | 68.00 |
| search Test - plain | 5 | 68/95 | 71.58 | 18/38 | 47.37 | 50/57 | 87.72 | 1.54 | 339.51 | 45.50 |
| search Test - verbose | 5 | 63/95 | 66.32 | 63/95 | 66.32 | 0/0 | | 25.84 | 485.36 | 136.07 |
| Hamiltonian Path | 5 | 60/95 | 63.16 | 60/95 | 63.16 | 0/0 | | 0.37 | 530.39 | 58.02 |
| Weighted Spanning Tree | 5 | 58/95 | 61.05 | 58/95 | 61.05 | 0/0 | | 3.24 | 596.39 | 122.04 |
| Solitaire Forward | 5 | 55/95 | 57.89 | 55/95 | 57.89 | 0/0 | | 1.19 | 593.05 | 49.06 |
| Bounded Spanning Tree | 5 | 54/95 | 56.84 | 54/95 | 56.84 | 0/0 | | 7.43 | 413.63 | 70.11 |
| Hamiltonian Cycle | 5 | 51/95 | 53.68 | 51/95 | 53.68 | 0/0 | | 0.47 | 464.71 | 51.30 |
| Solitaire Backward | 5 | 47/95 | 49.47 | 33/76 | 43.42 | 14/19 | 73.68 | 0.30 | 552.11 | 71.72 |
| Towers Of Hanoi | 5 | 43/95 | 45.26 | 43/95 | 45.26 | 0/0 | | 6.28 | 478.30 | 169.96 |
| Blocked N-Queens | 5 | 40/95 | 42.11 | 36/76 | 47.37 | 4/19 | 21.05 | 1.57 | 590.04 | 193.59 |
| Social Golfer | 5 | 37/95 | 38.95 | 24/38 | 63.16 | 13/57 | 22.81 | 0.84 | 291.48 | 30.70 |
| Schur Numbers | 5 | 31/95 | 32.63 | 11/57 | 19.30 | 20/38 | 52.63 | 1.23 | 496.82 | 104.57 |
| Hashiwokakero | 5 | 26/95 | 27.37 | 0/0 | | 26/95 | 27.37 | 6.71 | 377.69 | 72.36 |
| Weighted Latin Square | 5 | 23/95 | 24.21 | 6/19 | 31.58 | 17/76 | 22.37 | 0.23 | 576.28 | 144.13 |
| 15-Puzzle | 5 | 17/95 | 17.89 | 17/95 | 17.89 | 0/0 | | 106.66 | 502.53 | 327.56 |
| Weight Bounded Dominating Set Suite | 5 | 15/95 | 15.79 | 15/95 | 15.79 | 0/0 | | 1.55 | 467.51 | 112.55 |
| Traveling Salesperson Suite | 5 | 12/95 | 12.63 | 12/95 | 12.63 | 0/0 | | 0.35 | 212.66 | 20.24 |
| Solitaire Backward 2 | 5 | 11/95 | 11.58 | 11/95 | 11.58 | 0/0 | | 5.32 | 330.89 | 101.55 |
| Car Sequencing | 5 | 7/95 | 7.37 | 7/95 | 7.37 | 0/0 | | 7.17 | 556.49 | 249.51 |
Results for SAT instances only
| Benchmark Class | # | Solved | % | min | max | avg |
|---|
| RLP-200 | 1 | 18/19 | 94.74 | 1.93 | 224.15 | 36.42 |
| Factoring | 2 | 36/38 | 94.74 | 0.63 | 297.74 | 53.55 |
| RLP-150 | 1 | 17/19 | 89.47 | 0.45 | 19.45 | 4.60 |
| verify Test - variable Search Space | 5 | 81/95 | 85.26 | 0.24 | 303.32 | 16.43 |
| Knights Tour | 5 | 71/95 | 74.74 | 1.04 | 248.97 | 28.29 |
| Su-Doku | 3 | 42/57 | 73.68 | 18.15 | 176.69 | 68.00 |
| Random Non-Tight | 3 | 41/57 | 71.93 | 0.59 | 518.08 | 143.83 |
| search Test - verbose | 5 | 63/95 | 66.32 | 25.84 | 485.36 | 136.07 |
| Social Golfer | 2 | 24/38 | 63.16 | 0.87 | 291.48 | 25.21 |
| Hamiltonian Path | 5 | 60/95 | 63.16 | 0.37 | 530.39 | 58.02 |
| Weighted Spanning Tree | 5 | 58/95 | 61.05 | 3.24 | 596.39 | 122.04 |
| Solitaire Forward | 5 | 55/95 | 57.89 | 1.19 | 593.05 | 49.06 |
| Bounded Spanning Tree | 5 | 54/95 | 56.84 | 7.43 | 413.63 | 70.11 |
| Hamiltonian Cycle | 5 | 51/95 | 53.68 | 0.47 | 464.71 | 51.30 |
| search Test - plain | 2 | 18/38 | 47.37 | 1.54 | 339.51 | 42.52 |
| Blocked N-Queens | 4 | 36/76 | 47.37 | 1.57 | 590.04 | 191.26 |
| Towers Of Hanoi | 5 | 43/95 | 45.26 | 6.28 | 478.30 | 169.96 |
| Solitaire Backward | 4 | 33/76 | 43.42 | 1.50 | 552.11 | 100.61 |
| Weighted Latin Square | 1 | 6/19 | 31.58 | 0.23 | 6.70 | 1.61 |
| Schur Numbers | 3 | 11/57 | 19.30 | 65.40 | 437.76 | 191.95 |
| 15-Puzzle | 5 | 17/95 | 17.89 | 106.66 | 502.53 | 327.56 |
| Weight Bounded Dominating Set Suite | 5 | 15/95 | 15.79 | 1.55 | 467.51 | 112.55 |
| Traveling Salesperson Suite | 5 | 12/95 | 12.63 | 0.35 | 212.66 | 20.24 |
| Solitaire Backward 2 | 5 | 11/95 | 11.58 | 5.32 | 330.89 | 101.55 |
| Car Sequencing | 5 | 7/95 | 7.37 | 7.17 | 556.49 | 249.51 |
Results for UNSAT instances only
| Benchmark Class | # | Solved | % | min | max | avg |
|---|
| RLP-200 | 4 | 71/76 | 93.42 | 0.25 | 465.69 | 67.16 |
| RLP-150 | 4 | 70/76 | 92.11 | 0.25 | 183.29 | 16.50 |
| Random Non-Tight | 2 | 34/38 | 89.47 | 0.41 | 447.16 | 99.12 |
| search Test - plain | 3 | 50/57 | 87.72 | 6.46 | 126.01 | 46.57 |
| Factoring | 2 | 33/38 | 86.84 | 2.94 | 549.80 | 75.59 |
| Solitaire Backward | 1 | 14/19 | 73.68 | 0.30 | 6.67 | 3.62 |
| Schur Numbers | 2 | 20/38 | 52.63 | 1.23 | 496.82 | 56.51 |
| Hashiwokakero | 5 | 26/95 | 27.37 | 6.71 | 377.69 | 72.36 |
| Social Golfer | 3 | 13/57 | 22.81 | 0.84 | 266.83 | 40.85 |
| Weighted Latin Square | 4 | 17/76 | 22.37 | 0.30 | 576.28 | 194.43 |
| Blocked N-Queens | 1 | 4/19 | 21.05 | 51.32 | 546.50 | 214.59 |
|