Tableaux 2000 - Easy/medium benchmarks

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

Here we evaluate *SAT+USB performance, i.e., *SAT plus 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