Tableaux 2000 benchmarks, logic K

January 2000

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:
  • C are the of 4-literal clauses in the original QBF
  • D are the alternations of quantifiers
  • V is the maximum number of variables under the scope of each quantifier
  • mod denotes that propositional variables in the test are encoded into modal formulas in such a way that only one propositional variable survives.
Three different versions of *SAT are under evaluation:
  • *SAT this is the plain SAT-based algorithm for logic K.
  • *SAT+USB this adds bit-matrix based caching; its distinguishing features are:
    • it can store sets of formulas encoded as sets of integers
    • it can query for subsets (supersets)
    • it can be bounded in size and, if bounded, it allows to use a FIFO politic to discharge obsolete reults
  • *SAT+USH this adds hash-table based caching; its distinguishing features are:
    • it can store sets of formulas encoded as sets of integers
    • features a simple and fast exact-matching access
    • it never forgets results
For each algorithm we show the geometric mean of the Cpu time taken to solve some samples of each problem. A timelimit of 1200 seconds is enforced. >1200 in the table, means that all the samples exceeded the timelimit. Also the geometric mean of the number of Consistency checks is shown. For the samples that exceeed the timelimit we take into account the number of checks performed so far.

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
C10-V4-D4-mod >1200 4355018 30.20 20398 101.46 98330
C20-V4-D4-mod >1200 4014061 28.99 12796 176.98 134319
C30-V4-D4-mod >1200 3902022 48.49 28928 456.25 258761
C10-V4-D6-mod >1200 3707478 133.06 36251 155.37 140415
C20-V4-D6-mod >1200 3252054 787.94 487360 1038.93 671376
C10-V8-D4-mod >1200 3147085 795.03 157570 >1200 500019
C20-V8-D4-mod >1200 2548269 >1200 262289 >1200 313329
C30-V8-D4-mod >1200 2383854 1021.58 183388 >1200 218947

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.


Back to the state of the art page