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.
Four different versions of *SAT+USB are under evaluation each one
with a different window size, i.e., a different amount of
tests that can be stored without any previous result being
overwritten. In particular, w32 is the minimum size
allowed, w1024 is the biggest size that we find convenient
and w256, w512 are intermediate values that we use
to understand the persistency/search time tradeoff.
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 exceded the timelimit. Also the geometric mean of the
number Consistency checks is shown. For the samples that
exceeed the timelimit we take into account the number of checks
performed so far.
|