Solvers submission

Authors of the solvers will be required to register to the QBFLIB/QBFEVAL web portal starting from the September 1st, 2009, and they will be able to submit their solver(s), or update their submission, until October 15th, 2009. 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 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. However, submission of the source code will be mandatory unless participants can provide us with a compiled ELF-32 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.

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 August 31st, 2009.
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.
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.

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 submission

Authors of the instances/generators will be required to register to the QBFLIB/QBFEVAL web portal starting from the September 1st, 2009, and they will be able to submit their instances until October 15th, 2009. 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'10 the authors implicitly grant permission to the maintainers of QBFLIB to store and redistribute their work.

Rules

The test set of QBFEVAL'10 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 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 Sytems 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'10 will run on a farm of 9 identical PCs, available in the computing infrastructure of the MIND laboratory at the University of Genoa, equipped with a processor Intel Core 2 Duo @ 2.13 GHz, 4 Gb of RAM, running GNU Linux Debian 2.6.18.5.