QBFEVAL'18

Competitive evaluation of QBF solvers

A joint event with SAT 2018 - 21th Int. Conference on Theory and Applications of Satisfiability Testing (SAT) (affiliated with FLoC 2018)

Oxford, UK, July 9 - July 12 2018

QBFEVAL'18 is the 2018 competitive evaluation of QBF solvers, and the thirteenth evaluation of QBF solvers and instances ever. QBFEVAL'18 awards 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'18, please get in touch with the organizers via qbf18@qbflib.org.

Important Dates

  • Registration open: March 14 (for all tracks)
  • Registration close: April 7 April 22
  • Solvers and Benchmarks due: April 14 April 25 (for all tracks except Hard-Instances Track)
  • First stage results: April 30 May 3
  • Second stage solvers due: May 10 May 15 (for all tracks except Hard-Instances Track)
  • Hard instances solver due: June 1 (no registration is necessary)
  • Competition Benchmarks available for download: June 14
  • Final results: presented at SAT'18

QBFEVAL'18 Tracks

  1. Prenex CNF
  2. Prenex non-CNF
  3. 2QBF
  4. DQBF Solvers
  5. Hard-Instances Track

Submission guidelines and rules

Solvers registration and submission

Authors of the solvers are required to register for QBFEVAL'18 (for the deadlines see above) in Easychair. Authors have to provide a short abstract briefly describing the planned submission(s).

Each author/team can submit up to three solvers (except for the hard-instances track which allows only one submission per team/author), including different configurations/versions/flavors of the same solver (e.g., QuBE-BJ and QuBE-Rel would be considered as two different solvers).

Further submission instructions will be communicated to each registered person.

NEW!
  • The source code of the participating tool has to be publicly available.
  • The binaries submitted to the competition have to be made publicly available.
  • For the participating tool, an expressive tool description has to be made publicly available documenting the used solving techniques, external tools and configuration.
  • If the solver consists of multiple tools, then there should be one documented position where the paths to the used tools can be set, i.e., for calling a tool "mytool" in a script don't use "./mytool", but define a variable $MPATH and call "$MPATH/mytool".

The fulfillment of these requirements will be checked by the organizers. 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.

As in the year before, there will be a two-stage evaluation process. In the first stage, the solvers are tested with "easy" instances to identify problems of any kind. The problems will be reported to the submitters. Then resubmission of the fixed version is possible until the deadline (see above). For the second stage, there will be no intermediate feedback. The results will be announced at SAT'18.

If a track has less than three submissions from different research groups, the track will be canceled.

Formulas registration and submission

Authors of the instances/generators are required to register to QBFEVAL'18 in Easychair.

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 qbf18@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'18 the authors implicitly grant permission to the maintainers of QBFLIB to store and redistribute their work.

General Rules

The test set of QBFEVAL'18 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)".

For each track, a first, a second, and a third price will be awarded.

Per track, an author/a team of author can win only one price at most. If two submissions of a team win the first and second price for example, then the team will only be awarded the first price.

Infrastructure

It is planned to perform the QBFEVAL'18 using the computing infrastructure made available by StarExec. Specifications are available here, while a virtual machine image is available here.

As it has to be expected that StarExec will be very busy in spring 2018, because many competitions are affiliated with FLoC 2018, alternative computing infrastructures might be used. A change of infrastructure will be announced to the participants.

Prenex CNF Track

The requirements for the solvers are the following:

  • 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").
  • NEW! A special award will be provided to the solver that provides the most partial certificates of truth/falsity on standard output according to QDIMACS 1.1 output format that are correct.

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.

NEW! This year, two input formats are allowed: the QCIR format and the QAIGER format.

Submitted solvers have to support only one of the formats. For the QCIR format, solvers may assume the input formulas to be in the syntactically restricted cleansed format (see QCIR format).

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 instances must have the extension ".qcir.gz" indicating a text file in QCIR input format compressed with the utility program gzip.
  • NEW! Alternatively, the instances must have the extension ".aig.gz" indicating a text file in QAIGER input format compressed with the utility program gzip.
  • The instance must be formatted according to the QCIR input format or according to the QAIGER input format.

A tool for converting between QAIGER and QCIR is available at  https://github.com/ltentrup/quabs (many thanks to Leander Tentrup).

2QBF Track

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:

NEW! This year only dedicated 2QBF solvers are eligible for participation in the 2QBF track. Solvers that participate in any other track are automatically excluded from the 2QBF track.

DQBF Solvers

DQBF is a generalization of QBF that allows Henkin quantifiers. 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 DQDIMACS format. Details on DQDIMACS can be found at http://forsyte.at/wp-content/uploads/idq_pos2014.pdf.

Hard-Instances Track

NEW! In the Hard-Instances Track (HIT), we invite the participants to solve instances of the previous QBFEVAL that were too hard for any solver. These benchmarks are available http://www.qbflib.org/HARD_QDIMACS_QBFEVAL17.zip (when the call is officially published)

Only these benchmarks will be considered in HIT. Further, the following HIT-specific rules apply:

  • Only one system/configuration is allowed per author/team.
  • Resource limit might be increased (depending on availability) for this track. The submitters are invited to recommend limit which they found useful.
  • The track will be organized if there is at least one submission.
  • The submission deadline is after the deadline of the other tracks, but like for all other tracks, the intend to submit has to be expressed by registering the solver in the registration period.
  • This track has only an one-stage process, i.e., there will be no additional feedback round with easy instances. In case there are installation issues, the authors will be directly contacted by the organizers.

Organizing committee

Organization

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

Judges

Olaf Beyersdorff, University of Leeds
Christoph Wintersteiger, Microsoft Research Limited

Last update: 13-Apr-2018.