QBFEVAL'19 is the 2019 competitive evaluation of QBF solvers, and the fourteenth event aimed to assess the performance of QBF solvers. QBFEVAL'19 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'19, please get in touch with the organizers via qbfeval@qbflib.org.
Authors of the solvers are required to register for QBFEVAL'19 (for the deadlines see above) in Easychair (https://easychair.org/conferences/?conf=qbfeval19). 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.
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’19.
Authors of the instances/generators are required to register to QBFEVAL'19 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 qbfeval@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'19 the authors implicitly grant permission to the maintainers of QBFLIB to store and redistribute their work.
The test set of QBFEVAL'19 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 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. If a track has less than three submissions from different research groups, the track will be canceled.
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’18, 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:
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