Solvers submission

Authors of the solvers will be required to register to the QBFLIB/QBFEVAL web portal starting from the February 15th, 2012, and they will be able to submit their solver(s), or update their submission, until April 15th, 2012. Registration to the web portal will enable the participants to submit their solvers and to download a pool of instances having a certified satisfiability result. Shortly after the registration, participants will receive an acknowledgement message containing a login, a password, and the instructions to log into the QBFLIB/QBFEVAL portal. Such account can be used to upload the solver (either compiled, or using a specifically formatted source package). The mail should also contain a second account, login and password to connect to the system at CINECA where the solver can be compiled if participants do not want to submit a source code or their own Power6 binaries. Detailed compiling instructions could be found at CINECA. The solver will be compiled (if necessary) and checked for compliance with the requirements for the evaluation. Participants will receive a message confirming a successful submission or prompting for problems. Notice that we do not enforce submission of the source code, and the source code compiled on the target machine will be not public available. However, submission of the source code will be mandatory unless participants can provide us with a compiled xcoff64 executable for AIX (IBM Power 6 processor) (statically linked), or a set of .class java files (in a .jar archive)(java version available is 1.5.0). Scripts written in some mainstream language like Perl, Python, devoted to coordinate a pool of executables are also accepted. The requirements for the solvers are the following:

1. Each author can submit up to three solvers, including different versions/flavors of the same solver (e.g., QuBE-BJ and QuBE-Rel would be considered as two different solvers). Organizers are allowed to submit solvers in the competition division no later than the April the 15th 2012.
2. The solver must take exactly two command line input, i.e., the file containing the QBF instance to be processed and the granted CPU time limit (in seconds).
3. The solver must run as a single process (or a batch of processes).
4. The solver must read instances using the QDIMACS 1.1 input format. For this year you could assume that no free variables will be present in any benchmark. SAT benchmarks, if any, will be converted having an existential line of prefix variables.
5. 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").
6. The solver must kill itself when the time limit is exceeded; this includes any child process or executables that have been spawned or fired during the solution process.
7. The solver can output additional information and a partial certificate of truth/falsity on standard output according to QDIMACS 1.1 output format.
8. Finally, each solver must be accompanied by a system description in pdf format, max 2 pages in LNCS format. 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 submission

Authors of the instances/generators will be required to register to the QBFLIB/QBFEVAL web portal starting from the February 15th, 2012, and they will be able to submit their instances until April 15th, 2012. Registration to the web portal will enable unregistered participants to submit their instances. Shortly after the registration, participants will receive an automatically generated acknowledgement message containing a login, a password, and the instructions to log into the QBFLIB/QBFEVAL portal. Such account can be used to upload the instances. The instances will be (automatically) checked for compliance with the requirements for the evaluation. Submitters will receive a message with a log of the process, confirming a successful submission or prompting for problems.

The requirements for the QBF instances are the following:

1. The instance must have the extension ".qdimacs.gz" indicating a text file in QDIMACS 1.1 format compressed with the utility program gzip.
2. The instance must be formatted according to the QDIMACS 1.1 input format (this includes the instances produced by generators).
3. Each "group" of instances must be accompanied by a description in pdf format, max 2 pages in LNCS format.

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'12 the authors implicitly grant permission to the maintainers of QBFLIB to store and redistribute their work.

Rules

The test set of QBFEVAL'12 will be a selection of QBF encodings (no randomly generated formulas), 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[1];
• syntactic features [2];
• structural features [1];
• Solution (SAT/UNSAT), based on results of past QBFEVALs.

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.

For each selected formula, we are considering to compute a satisfiability-preserving shuffling of the formula involving variables in the prefix, literals in the clauses and clauses in the matrix.

We set the CPU time limit to 1200 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 2GB. If a solver ever exceeds this bound while solving a formula, it will be considered as a memory out. At the time of writing the rules we are not sure about memory limit, it could increse depending on the architecture used.

At the end of the competition, we will rank the solvers using the YASMv2 [6] scoring method, but we will also write a report about the results that includes other measures of merit/performances.

[1] L. Pulina and A. Tacchella. Treewidth: a useful marker of empirical hardness in quantified Boolean logic encodings. In proc. of LPAR 2008.
[2] L. Pulina and A. Tacchella. A self-adaptive multi-engine solver for quantified Boolean formulas. Constraints, 14(1):80-116, 2009.
[3] M. Narizzano, L. Pulina, and A. Tacchella. Ranking and Reputation Systems in the QBF competition. In 10th Conference of the Italian Association for Artificial Intelligence (AI*IA 2007), volume 4733 of Lecture Notes in Artificial Intelligence, pages 97-108. Springer-Verlag, 2007.

Infrastructure

QBFEVAL'12 will run on SP6/5376 infrastructure provided by Cineca, currently the most powerful computer in Italy. It is composed by 5376 IBM Power6, 4.7 GHz, cores, and it is capable of 101 TFlops (100 thousand billion operations per second). More informations can be found at http://www.cineca.it/en/hardware/ibm-sp65376-0