These benchmarks are described at the Tableaux 2000 competition homepage. They consist of modal formulas obtained by translating randomly generated quantified boolean formulas. For each test:
Here we evaluate *SAT+USB performance, i.e., *SAT plus bit-matrix based caching; its distinguishing features are:
|
Test | *SAT+USB | |||
---|---|---|---|---|
S/U/T | Cpu | Cons | Mem | |
C10-V4-D4 | 8/0/0 | 0.36 | 750 | 1501 |
C20-V4-D4 | 4/4/0 | 1.64 | 2231 | 1736 |
C10-V4-D6 | 8/0/0 | 0.50 | 973 | 1691 |
C30-V4-D4 | 3/5/0 | 2.83 | 2871 | 1830 |
C20-V4-D6 | 8/0/0 | 4.86 | 5279 | 2102 |
C40-V4-D4 | 1/7/0 | 4.43 | 3461 | 1879 |
C30-V4-D6 | 5/3/0 | 22.85 | 16895 | 2449 |
C50-V4-D4 | 0/8/0 | 4.41 | 3163 | 2451 |
C10-V8-D4 | 8/0/0 | 0.77 | 1302 | 2219 |
C40-V4-D6 | 1/7/0 | 33.29 | 18658 | 3307 |
C20-V8-D4 | 8/0/0 | 12.77 | 10773 | 3230 |
C10-V8-D6 | 8/0/0 | 0.78 | 1258 | 2666 |
C50-V4-D6 | 0/8/0 | 46.07 | 21509 | 3353 |
C30-V8-D4 | 8/0/0 | 92.74 | 49964 | 4035 |
C20-V8-D6 | 8/0/0 | 22.59 | 16482 | 4139 |
C40-V8-D4 | 2/5/1 | 517.84 | 203594 | 4384 |
C30-V8-D6 | 5/0/3 | 681.74 | 296324 | 5988 |
C50-V8-D4 | 0/3/5 | 197.68 | 71422 | 5582 |
C40-V8-D6 | 0/0/8 | -- | 380903 | -- |
C50-V8-D6 | 0/0/8 | -- | 309856 | -- |
C10-V16-D4 | 8/0/0 | 1.29 | 1840 | 3850 |
C20-V16-D4 | 8/0/0 | 75.98 | 45052 | 5095 |
C10-V16-D6 | 8/0/0 | 1.75 | 2064 | 4850 |
C30-V16-D4 | 6/0/2 | 703.53 | 244983 | 7068 |
C20-V16-D6 | 8/0/0 | 54.70 | 25887 | 6679 |
C40-V16-D4 | 0/0/8 | -- | 307407 | -- |
C30-V16-D6 | 5/0/3 | 502.92 | 152995 | 9720 |
C50-V16-D4 | 0/0/8 | -- | 261662 | -- |
C40-V16-D6 | 0/0/8 | -- | 253395 | -- |
C50-V16-D6 | 0/0/8 | -- | 180169 | -- |
Back to the state of the art page |