QBFEVAL'16 will be the 2016 competitive evaluation of QBF solvers, and the eleventh evaluation of QBF solvers and instances ever. QBFEVAL'16 will award solvers that stand out as being particularly effective on specific categories of QBF instances. The evaluation will run using the computing infrastructure made available by StarExec.
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. People 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'16, please get in touch with qbf16@qbflib.org.
Authors of the solvers will be required to register
to QBFEVAL'16 starting from February 1st, 2016,
in Easychair. Registration closes February 29th March 7th,
2016. Authors have to provide a short abstract briefly describing the
planned submission(s). Submission instructions will communicated to
each registered person.
For competitive tracks, authors of solvers will be
able to submit their solver(s), or update their submission in Easychair until
March 1st March 7th, 2016. From March 2nd to March 7th March 8th to March 13th, solvers will be checked
for compliance with the requirements for the evaluation. Participants
will receive a message confirming a successful submission or prompting
for problems. In the case of problems, participants can submit a fixed
version until March 15th March 22nd.
Authors of tools registered for non-competitive tracks can submit/update their system(s) until April 30th, 2016.
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 .class java 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.
We will not check the solvers for correctness any further, and during the evaluation the solvers giving a certifiable incorrect answer will be excluded (i.e., run hors concours).
Formulas registration and submissionAuthors of the instances/generators will be required
to register to QBFEVAL'16 starting from February 1st, 2016, in Easychair. Registration closes February 29th March 7th,
2016. 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 qbf16@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'16 the authors implicitly grant permission to the maintainers of QBFLIB to store and redistribute their work.
RulesThe test set of QBFEVAL'16 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 600 seconds. This should encourage researchers to submit their solvers, also if they are in a prototypical version. To prevent the memory swapping, we set the memory limit at 4GB. If a solver ever exceeds this bound while solving a formula, it will be considered as a memory out.
At the end of the competition, solvers will be ranked according to the total amount of solved formulas and, in the case of ties, to the CPU time spent. Special awards will be given to the best "State of the Art Contributor(s)".
InfrastructureQBFEVAL'16 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.
About 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.
About 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:
Aim of this track is to evaluate incremental QBF solvers. Incremental solving, as stated in (Lonsing and Egly, CP 2014), "aims at using information learned from one formula in the process of solving the next formulae in the sequence.".
About solvers and formulas submission, the same indications given for the Prenex CNF Track apply also to this track.
Aim of this non-competitive track is to assess the current state of the art about the certification of QBFs. About tools and formulas submission, the indications of the Prenex CNF Track apply also in this case, with the exception of the output format. For details, please contact the organizers at qbf16@qbflib.org.
In this track it will be evaluated QBF systems portfolios. Input and output format of solvers and formulas are the same of the Prenex CNF Track.
Aim of this non-competitive track is to assess the current state of the art about parallel QBF solvers. In this track will participate solvers accepting formulas in QDIMACS and/or in QCIR. The number of cores available for each solver is 4. For details, please contact the organizers at qbf16@qbflib.org.
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.