QBF Gallery 2013

News

Important Dates

  • 2013-04-02: registration open
  • 2013-04-15: registration closed
  • Due 2013-04-30: final submission
  • May, June 2013: evaluation runs
  • July 8 - 12 2013: presentation of results

Event affiliated to
SAT 2013 and QBF 2013

July 8-12 2013, Helsinki, Finland.

Call for Contributions

Call in ASCII text

Quantified Boolean formulas (QBF) are an extension of propositional logic which allows for explicit quantification over propositional variables. The decision problem of QBF is PSPACE-complete compared to NP-completeness of the decision problem of propositional logic (SAT).

Many problems from application domains such as model checking, formal verification or synthesis are PSPACE-complete, and hence could be encoded in QBF. Considerable progress has been made in QBF solving throughout the past years. However, in contrast to SAT, QBF is not yet widely applied to practical problems in industrial settings.

General Description

The QBF Gallery is an adjunct of the QBF Workshop 2013 that will be held in conjunction with SAT 2013.

The goal of the QBF Gallery is to empirically assess the state-of-the-art in QBF solving as well as collect and select expressive benchmarks. QBF researchers and users are invited to contribute their solvers, tools, and benchmarks to be used for evaluation. Submission of new benchmarks related to QBF applications which have been shown to be hard for QBF solvers in the past are particularly welcome.

Participants in the QBF Gallery will have the opportunity to actively take part in the selection of benchmarks and evaluation runs in a discussion group (further details will be sent to the participants after registration; see Section "Discussion Group" below). The actual schedule of evaluation runs and the benchmarks selection depend on the number and types of submitted systems and on available computational resources.

DISCLAIMER: The QBF Gallery is no typical competition but has competitive aspects. There will be no prizes and no officially announced winners. Therefore this event is called a "gallery".

The overall exhibition of the results of the QBF Gallery will be staged during the SAT 2013 conference, July 8 - 9.

The results of QBF Gallery will be summarized in an informal technical report to be published at this website. Additionally, participants may decide to contribute to (and hence be co-authors of) a journal version of this report (see Section "Publication" below).

Although the QBF Gallery is not a competitive event, there will be several evaluations of submitted tools, including tools not considered in the QBFEVAL series, such as solvers that produce certificates, verifiers for certificates, post-processors to extract a strategy from a proof, etc.

If available, new benchmarks submitted by participants as well as benchmarks from QBFLIB which have not been used during previous editions of QBFEVAL will be considered for evaluation runs.

Submission Procedure

Submission of contributions to the QBF Gallery consists of the following steps:

  1. Starting from April 2 2013, participants send an email with subject "QBF Gallery: registration request" briefly describing the type of the planned contributions (e.g. what kind of solver, application domain of benchmarks,...) to qbf2013@easychair.org due April 15 2013.
  2. Organizers will confirm registration by email and send detailed instructions regarding submission and access to discussion group (see Section "Discussion Group" below).
  3. Registered participants submit their contributions as instructed by the organizers due April 30 2013.

IMPORTANT:

  • Submitted tools and benchmarks will not become publicly available from the organizers (neither to the other participants).
  • Linux x86 (64 bit) is the standard platform on which all tools are expected to operate.
  • Tools may be submitted as source code or as statically linked binaries. If a participant wants to be co-author of the formal report of the QBF Gallery (see Section "Publication" below), then submission of source code is required.

      • Types of Submissions

      QBF Gallery is open to all kind of submissions related to evaluating and applying QBF including but not limited to:

      • CNF solvers
      • Non-CNF solvers
      • 2QBF solvers
      • Preprocessors
      • Certification tools
      • Certificate reduction tools
      • Benchmark generators
      • Sets of benchmark formulas
      • Scoring and evaluation methods

      Publication

      The results of the QBF Gallery will be published as an informal technical report available from the QBF Gallery website.

      A formal report is planned in the form of a paper to be submitted to ACM Journal on Experimental Algorithmics (JEA), for experiments involving tools for which source code is provided. Every participant who contributes source code and a structured brief description of the tool (along the lines of the SAT 2013 Competition) will be eligible to be an author of this version of the report.

      Discussion Group

      A novel feature of QBF Gallery (at least, novel for events in past SAT conferences) is that participants will join a Google group (unless they choose not to). Through the Google group, participants will discuss how to conduct and structure various evaluation runs and how to organize benchmark selection. The group will jointly form a suite of benchmarks for the evaluation runs and will discuss other evaluation issues. E.g. one goal is to solve instances that were previously unsolved or solved by only one solver.

      Access to the discussion group will be granted to registered participants. Participants will receive further details related to the discussion group by email after registration (see Section "Submission" above).

      Benchmark Selection and Scoring

      Another novel feature of QBF Gallery is the plan, subject to amendment, that the suite of instances for each round will be selected using a random procedure in which no one person controls which instances are selected. This procedure allows for the universe of benchmarks to be known during the event.

      A suite of publicly available preprocessors might be used to filter out benchmarks which can be solved solely by preprocessing. The details of this filtering process are subject to public discussions among the participants.

      There will be no prizes and no officially announced winners. Since evaluation methods are part of the contributed tools, there may be several scoring methods used on the results. By sparse but stratified sampling of a large benchmark universe, the amount of computation can be scaled to available resources, and there can be several passes.

      Possible Types of Evaluation Runs

      Which types of runs actually take place depends on what tools are submitted, on available resources, and on the outcome of the discussions of the participants.

      To the extent possible there will be warm-up runs so all tools can be exercised and improved before moving to longer rounds. Due to sampling, several equivalent final rounds are planned, rather than a single round. All results will be made available to participants as soon as possible.

      Depending on submissions, the types of runs might include solving QBF without a certificate, solving QBF with the QDIMACS partial certificate and solving QBF with a complete certificate for which a verifier is available.

      The types of runs might include special instances such as 2-level QBF (2QBF) and non-PCNF formulas. Also, various encodings from a common application might be used.

      The types of runs may include producing and verifying certificates of instances. We hope to have multiple verifiers for each certificate language, and multiple solvers for each certificate language. For sufficiently similar languages, translators might be provided.

      Contact

      qbf2013@easychair.org

      Organizers