QBFEVAL'17

Competitive evaluation of QBF solvers

A joint event with SAT 2017 - 20th International Conference on Theory and Applications of Satisfiability Testing

Melbourne, Australia, 28 August - 1 September 2017

QBFEVAL'17 will be the 2017 competitive evaluation of QBF solvers, and the twelfth evaluation of QBF solvers and instances ever. QBFEVAL'17 will award solvers that stand out as being particularly effective on specific categories of QBF instances.

We warmly encourage developers of QBF solvers to submit their work, even at early stages of development, as long as it fulfills some very simple requirements. We also welcome the submission of QBF formulas to be used for the evaluation.

Researchers thinking about using QBF-based techniques in their area (e.g., formal verification, planning, knowledge representation & reasoning) are invited to contribute to the evaluation by submitting QBF instances of their research problems (see the requirements for instances). The results of the evaluation will be a good indicator of the current feasibility of QBF-based approaches and a stimulus for people working on QBF solvers to further enhance their tools.

For questions, comments and any other issue regarding QBFEVAL'17, please get in touch with qbf17@qbflib.org.

Important Dates

  • Registration open: April 1st 2017
  • Registration close: May 22nd 2017
  • Solvers and Benchmarks due: May 30th 2017
  • First stage results: June 30th 2017
  • Second stage solvers due: July 7th 2017
  • Competition Benchmarks available for download: July 8th 2017
  • Final results: presented at SAT'17

QBFEVAL'17 Tracks

  1. Prenex CNF
  2. Prenex non-CNF
  3. 2QBF
  4. Parallel QBF Solvers
  5. Random QBFs
  6. Prenex CNF Preprocessors challenge
  7. DQBF Solvers

Submission guidelines and rules

Solvers registration and submission

Authors of the solvers will be required to register to QBFEVAL'17 starting from April 1st, 2017, in Easychair. Registration closes May 22th, 2017. Authors have to provide a short abstract briefly describing the planned submission(s). Submission instructions will be communicated to each registered person.

Authors of solvers will be able to submit their solver(s), update, and check for compliance with the requirements for the evaluation using StarExec until May 30th, 2017. In case of problems (e.g., discrepancies in the results), the organizers will send the details to the solvers authors by June 30th, 2017. All the participants can submit an updated/fixed version until July 7th, 2017.

Notice that we do not enforce submission of the source code. However, submission of the source code will be mandatory unless participants can provide us with a compiled executable for Linux (statically linked), or a set of java .class files (in a .jar archive). Scripts written in some mainstream language like Perl, Python, Ruby, devoted to coordinate a pool of executables are also accepted.

Solvers not complying to the above requirements will not be admitted to the evaluation. Notice that the solvers submitted to the evaluation will not be redistributed under any circumstances from the QBFLIB portal.

Formulas registration and submission

Authors of the instances/generators will be required to register to QBFEVAL'17 starting from April 1st, 2017, in Easychair. Registration closes May 22th, 2017. Authors have to submit a PDF description containing background information and an external link to the formulas. If you do not have webspace where you can put your formulas, please write an email to qbf17@qbflib.org. The instances will be checked for compliance with the requirements for the evaluation.

Please notice that the instances submitted to the evaluation will be made available for download on the QBFLIB portal. Therefore, by completing the submission to QBFEVAL'17 the authors implicitly grant permission to the maintainers of QBFLIB to store and redistribute their work.

Rules

The test set of QBFEVAL'17 will be a selection of QBF encodings, a part of which will be reserved to new submitted formulas. The remaining ones will be picked from the QBFLIB repository considering several parameters such empirical hardness, syntactic features, structural features, solution (SAT/UNSAT), and based on results of past events.

We will make sure that no more than 10% of the total test set comes from a single submitter whenever the formula submitter is also authoring a competing solver.

We set the CPU time limit to 900 seconds, and the memory limit at 32GB.

At the end of the competition, solvers will be ranked lexicographically according to the total amount of benchmarks solved (descending) and the total CPU time spent (ascending). Special awards will be given to the best "State of the Art Contributor(s)".

Infrastructure

QBFEVAL'17 will run using the computing infrastructure made available by StarExec. Specifications are available here, while a virtual machine image is available here.

Prenex CNF Track

The requirements for the solvers are the following:

  • Each author can submit up to three solvers, including different versions/flavors of the same solver (e.g., QuBE-BJ and QuBE-Rel would be considered as two different solvers).
  • The solver must be submitted with its configuration script for StarExec (see here for details).
  • The solver must run as a single process (or a batch of processes).
  • The solver must read instances using the QDIMACS 1.1 input format.
  • The solver must exit upon completion using exit code 10, if the instance is satisfiable, or exit code 20, if the instance is unsatisfiable (any other exit code is interpreted as "the instance could not be solved").
  • The solver can output additional information and a partial certificate of truth/falsity on standard output according to QDIMACS 1.1 output format.

The requirements for the QBF instances are the following:

  • The instance must have the extension ".qdimacs.gz" indicating a text file in QDIMACS 1.1 format compressed with the utility program gzip.
  • The instance must be formatted according to the QDIMACS 1.1 input format (this includes the instances produced by generators).
  • The instances must not be randomly generated.

Prenex non-CNF Track

The same indications given for the Prenex CNF Track apply also to this track, with the only exception of input and output format.

Regarding solvers, the same rules of QBF Gallery 2014 apply in this case, namely:

  • The input format for this track will be the QCIR format. This format supports Non-Prenex non-CNF quantified circuits.
  • Solvers may assume the input formulas to be in the syntactically restricted cleansed format (see QCIR format). If you have a solver which supports the full format, please contact the organizers at qbf17@qbflib.org.
  • For Prenex non-CNF solvers, the formulas will be provided in prenex normal form.
  • The only required output is the result of the solution process given in terms of exit-codes as described above.

Concerning the submission of instances, the requirements for the QBFs in QCIR input format are the following:

  • The instance must have the extension ".qcir.gz" indicating a text file in QCIR input format compressed with the utility program gzip.
  • The instance must be formatted according to the QCIR input format.

2QBF Track

Automated reasoning tasks encoded in 2QBF are frequently used, for instance, to encode conformant planning and property verification problems. Such problems could be solved by a general-purpose QBF solver, as well as special-purpose approaches like, e.g., cooperation of two state-of-the-art SAT solvers or encoding it into another logic, like, e.g. Disjunctive Logic Programming. The aim of this track is to attract participant from other Automated Reasoning communities in order to promote the cross-fertilization.

Regarding solvers and formulas submission, the same indications given for the Prenex CNF Track apply also to this track, with the only exception concerning the input format, which is a specialization of the standard QDIMACS format.

Considering the BNF grammar related to QDIMACS, the input format for the 2QBF track is described as follows:

Parallel QBF Solvers Track

The aim of this track is to assess the current state of the art about parallel QBF solvers. In this track will participate solvers accepting formulas in QDIMACS 1.1. The number of cores available for each solver is 24. Finally, because StarExec does not support the MPI libraries, the track will run on different infrastructure; details will be soon available.

For details, please contact the organizers at qbf17@qbflib.org.

Random QBFs Track

The aim of this track is to evaluate performances of state-of-the-art Prenex CNF QBF solvers on random instances. The requirements for solvers, formulas, and generators are the same given for Prenex CNF Track, with the exception that in this case submitted formulas must be randomly generated.

Prenex CNF Preprocessors challenge

The aim of this track is to evaluate (and award) the impact of preprocessing in the QBF solution process. In this track submissions of both preprocessors and solvers without any preprocessing systems will be accepted for QBF in QDIMACS1.1 format.

The evaluation process will be organized as follows. Given a set of submitted preprocessors P, a set of submitted solvers S, and a set of formulas F, the state-of-the-art (SOTA) system of S on F preprocessed by each p_i \in P will be computed. Preprocessors p_i will be ranked according to the total amount of instances solved by SOTA. Notice that F will not contain formulas solved directly by preprocessors on P.

About remaining indications on solvers and formulas submission, the same given for the Prenex CNF Track apply also to this track.

DQBF Solvers

The aim of this non-competitive track is to assess the current state of the art about DQBF solvers. The idea is collect systems and formulas available in order to organize a preliminary discussion on the general assessment of this kind of systems during the SAT conference. Further details will be soon available.

Organizing committee

Organization

Luca Pulina, University of Sassari
Martina Seidl, Johannes Kepler Universitat Linz

Judges

Olaf Beyersdorff, University of Leeds
Daniel Le Berre, Université d'Artois
Martin Suda, Technische Universität Wien
Christoph Wintersteiger, Microsoft Research Limited

Last update: 5-Mar-2017.