QBFEVAL'17 will be the 2017 competitive evaluation of QBF solvers, and the twelfth evaluation of QBF solvers and instances ever. QBFEVAL'17 will award 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'17, please get in touch with qbf17@qbflib.org.
Authors of the solvers will be required to register to QBFEVAL'17 starting from April 1st, 2017, in Easychair. Registration closes May 22th, 2017. Authors have to provide a short abstract briefly describing the planned submission(s). Submission instructions will be communicated to each registered person.
Authors of solvers will be able to submit their solver(s), update, and check for compliance with the requirements for the evaluation using StarExec until May 30th, 2017. In case of problems (e.g., discrepancies in the results), the organizers will send the details to the solvers authors by June 30th, 2017. All the participants can submit an updated/fixed version until July 7th, 2017.
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 java .class 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.
Formulas registration and submissionAuthors of the instances/generators will be required to register to QBFEVAL'17 starting from April 1st, 2017, in Easychair. Registration closes May 22th, 2017. 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 qbf17@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'17 the authors implicitly grant permission to the maintainers of QBFLIB to store and redistribute their work.
RulesThe test set of QBFEVAL'17 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)".
InfrastructureQBFEVAL'17 will run using the computing infrastructure made available by StarExec. Specifications are available here, while a virtual machine image is available here.
The requirements for the solvers are the following:
The requirements for the QBF instances are the following:
The same indications given for the Prenex CNF Track apply also to this track, with the only exception of input and output format.
Regarding solvers, the same rules of QBF Gallery 2014 apply in this case, namely:
Concerning the submission of instances, the requirements for the QBFs in QCIR input format are the following:
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.
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:
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 24. Finally, because StarExec does not support the MPI libraries, the track will run on different infrastructure; details will be soon available.
For details, please contact the organizers at qbf17@qbflib.org.
The 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.
The aim of this track is to evaluate (and award) the impact of preprocessing in the QBF solution process. In this track submissions of both preprocessors and solvers without any preprocessing systems will be accepted for QBF in QDIMACS1.1 format.
The evaluation process will be organized as follows. Given a set of submitted preprocessors P, a set of submitted solvers S, and a set of formulas F, the state-of-the-art (SOTA) system of S on F preprocessed by each p_i \in P will be computed. Preprocessors p_i will be ranked according to the total amount of instances solved by SOTA. Notice that F will not contain formulas solved directly by preprocessors on P.
About remaining indications on solvers and formulas submission, the same given for the Prenex CNF Track apply also to this track.
The aim of this non-competitive track is to assess the current state of the art about DQBF solvers. The idea is collect systems and formulas available in order to organize a preliminary discussion on the general assessment of this kind of systems during the SAT conference. Further details will be soon available.