QBFEVAL'22

QBFEVAL'22 - Competitive Evaluation of QBF Solvers



A joint event with the 25th Int. Conference on Theory and Applications of Satisfiability Testing (SAT, affiliated with FLoC 2022)


Haifa, Israel, August 2 - 5 2022


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

Important Dates

  • Registration deadline: March 25, 2022
  • Benchmarks due: April 1, 2022
  • Solvers due: April 29, 2022
  • First stage results: May 15, 2022
  • Second stage solvers due: May 30, 2022
  • Competition Benchmarks available for download: July 15, 2022
  • Final results: presented at SAT'22

QBFEVAL'22 Tracks

  • Prenex CNF
  • Crafted Instances Track (Prenex CNF)
  • Prenex non-CNF
  • DQBF Solvers
  • Parallel Track

Submission guidelines and rules

Solvers registration and submission

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

Formulas registration and submission

Authors of the instances/generators are required to register to QBFEVAL'22 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 mailto: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'22 the authors implicitly grant permission to the maintainers of QBFLIB to store and redistribute their work.

General Rules

The test set of QBFEVAL'22 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 authors 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'22 using the computing infrastructure made available by StarExec. Specifications are available here. The parallel track will be run on a cluster at JKU Linz (To be confirmed). For the details please contact Martina Seidl if you are interested in participating.

Prenex CNF Track and Crafted Instances Tracks

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. Submitted solvers have to support 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.
  • The instance must be formatted according to the QCIR input format.

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
Olaf Beyersdorff, University of Jena
Christoph Wintersteiger, Microsoft Research Limited