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.
The same indications given for the main competition 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:
At submission time, authors of solvers customized for 2QBF formulas will be required to state it by checking a box on the web submission form.
As for the main competitions, authors of solvers are allowed to submit at most three solvers.
Also for this track, we will set the CPU time limit to 1200 seconds and the memory limit at 2GB.
At the end of the evaluation, we will rank the solvers by the number of solved formulas and we will break ties using CPU time.