Last modified: 2013-07-23

Contributors

Solvers

• Sam Bayless: mini2qbf (2QBF solver)
• Alexandra Goultiaeva: ooq, dual_ooq + variants
• Mikolas Janota: rareqs
• Will Klieber: ghostQ + variants
• Florian Lonsing: nenofex, depqbf
• Massimo Narizzano: squeeze-qube3.0
• Allen Van Gelder: hiqqer

Preprocessors

• Armin Biere, Martina Seidl: bloqqer
• Massimo Narizzano: squeeze
• Allen Van Gelder: variants of hiqqer

Certification Frameworks

• Valeriy Balabanov, Jie-Hong R. Jiang: ResQu
• Aina Niemetz, Mathias Preiner: QBFcert

Benchmarks

• Michael Cashmore: Conformant Planning
• Martin Kronegger, Andreas Pfandler, Reinhard Pichler: Conformant Planning
• Charles Jordan, Lukas Kaiser: Reduction Finding
• Paolo Marin, Christian Miller: QBF Hardness
• Matthias Reimer, Sven Sauer: Fault Testing

Results

• Talk slides (short version) presented at the SAT conference 2013: PDF.
• Talk slides (long version) presented at the QBF Workshop 2013: PDF.
• Related poster presented at the SAT conference 2013: PDF.
• Results from the showcase "Preprocessing".
• Results from the showcase "Solving".
• Results from the showcase "Applications".
• Results from the showcase "Certificates".

Log-Files

• Log-files of experiments with solvers (47 MB).
• Log-files of experiments with preprocessing (7 MB).
• Log-files of experiments with certificates (2 MB).

Benchmarks

• Tool for benchmark sampling.

Newly Submitted Formulas

• README file describing the benchmarks which were submitted to the QBF Gallery 2013.
• conformant-planning (248 MB).
• planning-CTE (84 MB).
• qbf-hardness (3 MB).
• reduction-finding-full-set-params-k1c3n4 (77 MB).
• sauer-reimer (32 MB).

Formula Sets Used for Experiments

• eval2010 (187 MB).
• eval2012r2 (51 MB).
• eval2012r2-inc-preprocessed (58 MB).
• Sampling Experiment (1,5 GB).
• Application Formulas (2.3 GB).
• eval2012r2 preprocessed with bloqqer (26 MB).
• eval10 with bloqqer (64 MB) .