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-V16-D4 | 0/0/8 | -- | 274821 | -- |
C20-V16-D4 | 0/0/8 | -- | 128255 | -- |
C10-V16-D6 | 0/0/8 | -- | 245182 | -- |
C10-V4-D4 | 8/0/0 | 404.29 | 314270 | 2546 |
C20-V4-D4 | 2/0/6 | 851.98 | 491633 | 2675 |
C30-V4-D4 | 0/4/4 | 208.54 | 98368 | 2797 |
C10-V4-D6 | 0/0/8 | -- | 637938 | -- |
C20-V4-D6 | 0/0/8 | -- | 419442 | -- |
C40-V4-D4 | 0/8/0 | 133.40 | 55410 | 2903 |
C10-V8-D4 | 0/0/8 | -- | 460257 | -- |
C30-V4-D6 | 0/0/8 | -- | 339490 | -- |
C50-V4-D4 | 0/6/2 | 57.65 | 20764 | 3415 |
C40-V4-D6 | 0/0/8 | -- | 313328 | -- |
C20-V8-D4 | 0/0/8 | -- | 301734 | -- |
C50-V4-D6 | 0/0/8 | -- | 272332 | -- |
C30-V8-D4 | 0/0/8 | -- | 190460 | -- |
C10-V8-D6 | 0/0/8 | -- | 366596 | -- |
C20-V8-D6 | 0/0/8 | -- | 178572 | -- |
C40-V8-D4 | 0/0/8 | -- | 179803 | -- |
Back to the state of the art page |