Solvers and formulas submission

The same indications given for the main competition apply also to this track, with the only exception concerning the input and the output format. At submission time, authors of solvers must state explicitly whether their solver is meant to participate to the main track or to the non-prenex non-cnf track (solvers accepting both formats may participate in both tracks). As for the main competition, authors of solvers are allowed to submit at most three solvers.

The input format for this track will be the input format for the QBF solver qpro. The only required output is the result of the solution process given in terms of exit-codes as described in the main competition page.

You can download here the test set of the non-prenex non-cnf track of QBFEVAL'08 in qpro input format (thanks to Martina Seidl for the converter, that is available for download here).

Concerning the submission of instances, the requirements for the QBFs in qpro input format are the following:

1. The instance must have the extension ".qpro.gz" indicating a text file in qpro input format compressed with the utility program gzip.
2. The instance must be formatted according to the qpro 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.

Rules

The test set of this track will be a balanced selection of "structured" formulas, considering both the solution value and the empirical hardness parameters of formulas used in past non-prenex non-cnf evaluations.

Also for this track, we will set the CPU time limit to 1200 seconds and the memory limit at 2GB, as for the main competition.

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.