| These benchmarks are described at the homepage. They consist of modal formulas obtained by translating randomly generated quantified boolean formulas. MORE!!! |
| Test | *SAT | *SAT+USB | *SAT+USH | |||
|---|---|---|---|---|---|---|
| Cpu | Cons | Cpu | Cons | Cpu | Cons | |
| C10-V4-D4 | $>$1200 | 736535 | 102.05 | 26663 | 133.82 | 41898 |
| C20-V4-D4 | $>$1200 | 654802 | 321.15 | 75967 | 493.66 | 131996 |
| C30-V4-D4 | 157.71 | 98681 | 18.08 | 3953 | 29.36 | 8253 |
| C10-V4-D6 | $>$1200 | 533239 | 1103.23 | 181517 | $>$1200 | 202489 |
| C20-V4-D6 | $>$1200 | 507785 | $>$1200 | 152006 | $>$1200 | 32282 |
| C10-V8-D4 | $>$1200 | 379344 | $>$1200 | 109023 | $>$1200 | 125439 |
| C20-V8-D4 | $>$1200 | 396821 | $>$1200 | 66377 | $>$1200 | 78798 |
| C30-V8-D4 | $>$1200 | 339884 | $>$1200 | 55121 | $>$1200 | 64837 |
| As can be observed from the table, *SAT without caching is not able to solve most of the problem instances within the time limit. Caching produces dramatic speedups (up to two orders of magnitude) and, particularly, caching with a bit matrix yields the best results reducing consistency checks as well as Cpu time. |