QBFEVAL'20

QBFEVAL'20 - Competitive Evaluation of QBF Solvers

A joint event with the 23rd Int. Conference on Theory and Applications of Satisfiability Testing (SAT)

Alghero, Italy, July 5 - 9 2020

QBFEVAL'20 is the 2020 competitive evaluation of QBF solvers, and the fifteenth event aimed to assess the performance of QBF solvers. QBFEVAL'20 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'20, please get in touch with the organizers via qbfeval@qbflib.org.

Important Dates

  • Registration deadline: April 19 May 5, 2020
  • Solvers and Benchmarks due: April 26 May 10, 2020
  • First stage results: May 3 May 17, 2020
  • Second stage solvers due: May 17 May 24, 2020
  • Competition Benchmarks available for download: July 1, 2020
  • Final results: presented at SAT'20

QBFEVAL'20 Tracks

  1. Prenex CNF
  2. Crafted Instances Track (Prenex CNF)
  3. Prenex non-CNF
  4. DQBF Solvers
  5. Parallel Track

Submission guidelines and rules (Preliminary)

Solvers registration and submission

Authors of the solvers are required to register for QBFEVAL'20 (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 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.

  • As in previous editions of QBFEval, 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 previous editions, 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’20.

Formulas registration and submission

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

Authors have to submit a PDF description containing background information and an external link to the formulas. If you do not have a webspace where you can put your formulas, please write an email to qbfeval@qbflib.org. The instances will be checked for compliance with the requirements for the evaluation.

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

General Rules

The test set of QBFEVAL'20 will be a selection of QBF encodings, a part of which will be reserved for 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 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)". Depending on the submitted families, a special scoring scheme for the Crafted Instances Track will be applied. 

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 prize for example, then the team will only be awarded the first prize. If a track has less than three submissions from different research groups, the track will be canceled.

Infrastructure

It is planned to perform the QBFEVAL'20 using the computing infrastructure made available by StarExec. Specifications are available here. The parallel track will be run on a cluster at JKU Linz. For the details please contact Martina Seidl (martina.seidl@jku.at) if you are interested in participating.

Prenex CNF Track and Crafted Instances 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")
  • 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).
  • In the prenex CNF track only instances with a practical application domain (e.g., verification, planning, etc) will be considered. In the Crafted Instances Track, formula families specially designed for special purposes (e.g., showing the different strengths of proof systems) are considered (like the KBKF formula family or the parity formula family).  

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. As in QBFEVAL’19, 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.
  • 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).

DQBF Track

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

Parallel 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 at least 16.

Organizing Committee

Organization

Luca Pulina, University of Sassari

Martina Seidl, Johannes Kepler Universitat Linz

Ankit Shukla, Johannes Kepler Universitat Linz

Judges

TBA

Last update: 26-Feb-2020.