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 | 0/8/0 | 2.73 | 2708 | 3007 |
C20-V4-D4 | 0/8/0 | 6.89 | 4805 | 3399 |
C30-V4-D4 | 0/8/0 | 9.08 | 6383 | 3429 |
C10-V4-D6 | 0/8/0 | 2.18 | 1474 | 4129 |
C40-V4-D4 | 0/8/0 | 16.87 | 11012 | 3501 |
C20-V4-D6 | 0/8/0 | 7.66 | 4534 | 5441 |
C30-V4-D6 | 0/8/0 | 14.82 | 7395 | 5628 |
C50-V4-D4 | 0/8/0 | 20.87 | 14330 | 4027 |
C10-V8-D4 | 0/8/0 | 25.18 | 11868 | 6264 |
C40-V4-D6 | 0/8/0 | 21.95 | 10432 | 6506 |
C20-V8-D4 | 0/8/0 | 502.22 | 151215 | 9587 |
C10-V8-D6 | 0/8/0 | 53.73 | 20948 | 9938 |
C50-V4-D6 | 0/8/0 | 33.71 | 15513 | 6667 |
C30-V8-D4 | 0/6/2 | 570.79 | 159546 | 10852 |
C20-V8-D6 | 0/8/0 | 172.09 | 38982 | 16164 |
C40-V8-D4 | 0/3/5 | 655.53 | 164708 | 11309 |
C30-V8-D6 | 0/7/1 | 447.32 | 86268 | 20550 |
C50-V8-D4 | 0/2/6 | 934.99 | 199231 | 12379 |
C40-V8-D6 | 0/2/6 | 885.67 | 115207 | 22524 |
C50-V8-D6 | 0/2/6 | 1113.81 | 208242 | 24986 |
C10-V16-D4 | 0/0/8 | -- | 497959 | -- |
C20-V16-D4 | 0/0/8 | -- | 150031 | -- |
C10-V16-D6 | 0/3/5 | 375.51 | 95405 | 24267 |
Back to the state of the art page |