June/July 2013 ====================================================================== QBF Gallery 2013 Benchmarks ====================================================================== This file describes the benchmarks which were used for experimental runs in the course of the QBF Gallery 2013. Please see the event website for further information about the QBF Gallery: http://www.kr.tuwien.ac.at/events/qbfgallery2013/ ---------------------------------------------------------------------- Set 'reduction-finding-full-set-params-k1c3n4': 4608 formulas generated using a generator for instances from reduction finding, which is the problem to determine whether parametrized quantifier-free reductions exist between various decision problems in NL for one set of fixed parameters. These reductions are only required to be correct on structures of fixed-size (size 4 for the instances in the gallery) -- determining whether a reduction is correct/exists/etc. in general is of course undecidable. This is discussed in the following related papers. The generator was contributed by Charles Jordan and Lukasz Kaiser. Related papers: Charles Jordan and Lukasz Kaiser. Experiments with Reduction Finding. Proc. SAT 2013, LNCS 7962, pp. 192--207, 2013. Crouch, Immerman, Moss. Finding Reductions Automatically. LNCS 6300 (Gurevich Festschrift), pp. 181--200, 2010. Related links: The generator is available as the binary 'ReductionTest.native' in Toss >=0.9 (http://toss.sf.net), a Javascript version is available at http://toss.sf.net/reduct.html See also http://toss.sourceforge.net/reductGen.html for related information. The set of 4608 instances was generated with parameters k=1, c=3, n=4 and consists of 2304 + 2304 encodings of reduction problems where each problem is encoded twice: as 2QBF with prefix AE and additionally as a QBF with prefix EAE. ---------------------------------------------------------------------- Set 'eval2012r2': 345 formulas sampled from the collection of formulas available from QBFLIB at http://www.qbflib.org/. This set was also used for QBFEVAL 2012 Second Round. ---------------------------------------------------------------------- Set 'eval2012r2-inc-preprocessed': Instances from the benchmark set 'eval2012r2' (see above) which were obtained by incremental preprocessing using the four preprocessors that were submitted to the QBF Gallery 2013. We obtained the following two sets by incremental applications of preprocessing on the 345 instances from 'eval2012r2': Set 'eval2012r2-inc-preprocessed/ num-rounds-6-120sec-AABBCCDD-completion': 234 instances resulting from the set 'eval2012r2' by incremental preprocessing. From the 345 instances, 111 instances were solved during incremental preprocessing as follows: 6 rounds of incremental preprocessing, 120 seconds real time limit for each call of a preprocessor, execution ordering AABBCCDD, where "A" is hiqqer3e, "B" is bloqqer, "C" is hiqqer3p, and "D" is squeeze. Completion detection was enabled (i.e. preprocessing stops if the formula is no longer modified by any preprocessor). Set 'eval2012r2-inc-preprocessed/ num-rounds-6-120sec-AADDBBCC-completion': 241 instances resulting from the set 'eval2012r2' by incremental preprocessing. From the 345 instances, 104 instances were solved during incremental preprocessing as follows: 6 rounds of incremental preprocessing, 120 seconds real time limit for each call of a preprocessor, execution ordering AADDBBCC, where "A" is hiqqer3e, "B" is bloqqer, "C" is hiqqer3p, and "D" is squeeze. Completion detection was enabled (i.e. preprocessing stops if the formula is no longer modified by any preprocessor). Please see the event website for results and further information: http://www.kr.tuwien.ac.at/events/qbfgallery2013/ ---------------------------------------------------------------------- Set 'conformant-planning': 1750 instances from a planning domain with uncertainty in the initial state, contributed by Martin Kronegger, Andreas Pfandler, and Reinhard Pichler. Related paper: Martin Kronegger, Andreas Pfandler and Reinhard Pichler: Conformant Planning as a Benchmark for QBF-Solvers. Informal report of the QBF Workshop 2013, http://fmv.jku.at/qbf2013/index.html ---------------------------------------------------------------------- Set 'planning-CTE': 150 instances from QBF-based planning, contributed by Michael Cashmore. Related paper: Michael Cashmore, Maria Fox, Enrico Giunchiglia: Planning as Quantified Boolean Formula. ECAI 2012: 217-222. ---------------------------------------------------------------------- Set 'sauer-reimer': 924 instances from QBF-based test generation, contributed by Paolo Marin. Related paper: Sauer, M., Reimer, S., Polian, I., Schubert, T., Becker, B.: Provably optimal test cube generation using quantified boolean formula solving. In: ASP-DAC. (2013) to appear. See the PDF file 'sauer_reimer_bench_description.pdf' in the subdirectory for further information. ---------------------------------------------------------------------- Set 'qbf-hardness': 198 instances from bounded model checking of incomplete designs, contributed by Paolo Marin. Related paper: Christian Miller, Stefan Kupferschmid, Matthew D. T. Lewis, Bernd Becker: Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs. SAT 2010: 194-208. See the PDF file 'qbf-hardness-description.pdf' in the subdirectory for further information. ----------------------------------------------------------------------