QBFEVAL'16

Competitive evaluation of QBF solvers

A joint event with SAT 2016 - The Nineteenth International Conference on Theory and Applications of Satisfiability Testing

Bordeaux, France, July 5-8, 2016

QBFEVAL'16 will be the 2016 competitive evaluation of QBF solvers, and the eleventh evaluation of QBF solvers and instances ever. QBFEVAL'16 will award solvers that stand out as being particularly effective on specific categories of QBF instances. The evaluation will run using the computing infrastructure made available by StarExec.

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. People 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'16, please get in touch with qbf16@qbflib.org.

Important Dates

  • Registration open: February 1st 2016
  • Registration close: February 29th 2016 March 7th 2016
  • Solvers participating in competitive tracks due: March 1st 2016 March 7th 2016
  • Final versions of solvers participating in competitive tracks due: March 15th 2016 March 22nd 2016
  • Benchmarks due: March 15th 2016 March 22nd 2016
  • Solvers participating in non-competitive tracks due: April 30th 2016
  • Results: presented at SAT'16

QBFEVAL'16 Tracks

  1. Prenex CNF
  2. (Non-)Prenex non-CNF
  3. 2QBF
  4. Incremental Solvers
  5. Evaluate & Certify (non-competitive)
  6. Solver Portfolio
  7. Parallel QBF Solvers (non-competitive)
  8. Random QBFs

Submission guidelines and rules

Solvers registration and submission

Authors of the solvers will be required to register to QBFEVAL'16 starting from February 1st, 2016, in Easychair. Registration closes February 29th March 7th, 2016. Authors have to provide a short abstract briefly describing the planned submission(s). Submission instructions will communicated to each registered person.

For competitive tracks, authors of solvers will be able to submit their solver(s), or update their submission in Easychair until March 1st March 7th, 2016. From March 2nd to March 7th March 8th to March 13th, solvers will be checked for compliance with the requirements for the evaluation. Participants will receive a message confirming a successful submission or prompting for problems. In the case of problems, participants can submit a fixed version until March 15th March 22nd.

Authors of tools registered for non-competitive tracks can submit/update their system(s) until April 30th, 2016.

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 .class java 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.

We will not check the solvers for correctness any further, and during the evaluation the solvers giving a certifiable incorrect answer will be excluded (i.e., run hors concours).

Formulas registration and submission

Authors of the instances/generators will be required to register to QBFEVAL'16 starting from February 1st, 2016, in Easychair. Registration closes February 29th March 7th, 2016. 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 qbf16@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'16 the authors implicitly grant permission to the maintainers of QBFLIB to store and redistribute their work.

Rules

The test set of QBFEVAL'16 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 600 seconds. This should encourage researchers to submit their solvers, also if they are in a prototypical version. To prevent the memory swapping, we set the memory limit at 4GB. If a solver ever exceeds this bound while solving a formula, it will be considered as a memory out.

At the end of the competition, solvers will be ranked according to the total amount of solved formulas and, in the case of ties, to the CPU time spent. Special awards will be given to the best "State of the Art Contributor(s)".

Infrastructure

QBFEVAL'16 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 take exactly two command line input, i.e., the file containing the QBF instance to be processed and the granted CPU time limit (in seconds).
  • 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 must kill itself when the time limit is exceeded; this includes any child process or executables that have been spawned or fired during the solution process.
  • 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 istances must not be randomly generated.

(Non-)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.

About 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 qbf16@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.

About 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:

Incremental Solvers Track

Aim of this track is to evaluate incremental QBF solvers. Incremental solving, as stated in (Lonsing and Egly, CP 2014), "aims at using information learned from one formula in the process of solving the next formulae in the sequence.".

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

Evaluate & Certify Track

Aim of this non-competitive track is to assess the current state of the art about the certification of QBFs. About tools and formulas submission, the indications of the Prenex CNF Track apply also in this case, with the exception of the output format. For details, please contact the organizers at qbf16@qbflib.org.

QBF Solvers Portfolio Track

In this track it will be evaluated QBF systems portfolios. Input and output format of solvers and formulas are the same of the Prenex CNF Track.

Parallel QBF Solvers Track

Aim of this non-competitive track is to assess the current state of the art about parallel QBF solvers. In this track will participate solvers accepting formulas in QDIMACS and/or in QCIR. The number of cores available for each solver is 4. For details, please contact the organizers at qbf16@qbflib.org.

Random QBFs Track

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.

Organizing committee

Organization

Luca Pulina, University of Sassari

Judges

Hubie Chen, University of the Basque Country and Ikerbasque
Martina Seidl, Johannes Kepler Universitat Linz
Christoph Wintersteiger, Microsoft Research Limited

Last update: 12-Feb-2016.