-------------------------------------------------------------------------------------------------------------------------- QBFEVAL'08 -------------------------------------------------------------------------------------------------------------------------- Third competitive evaluation of QBF solvers A joint event with SAT 2008 - The Eleventh International Conference on Theory and Applications of Satisfiability Testing - May 12-15, 2008 - Guangzhou, P. R. China QBFEVAL'08 is the third competitive evaluation of QBF solvers, and the sixth evaluation of QBF solvers and instances ever. QBFEVAL'08 will award solvers that stand out as being particularly effective on specific categories of QBF instances and instances that turn out to be particularly hard to solve given the current state of the art. As in the previous event, QBFEVAL'08 will have also a track for solvers that take as input instances in non-prenex, non-cnf format. The evaluation starts on February and finishes by May 2008. The evaluation is run using the computing infrastructure made available by the MIND laboratory at the University of Genoa. The final results of the evaluation will be presented during SAT 2008. 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 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. Please notice that we are providing a test set of challenging formulas as well as a test set of certified satisfiable/unsatisfiable formulas. See here for more details. For questions, comments and any other issue regarding QBFEVAL'08, please get in touch with qbf08@qbflib.org Important Dates Registration (Participant) open January 15, 2008 Solvers and Instances due February 1, 2008 Evaluation runs February-May, 2008 Results May 12-15, 2008 Solvers submission Authors of the solvers will be required to register to the QBFLIB/QBFEVAL web portal (www.qbflib.org) no later than January 15, 2008. Registered users of QBFLIB will be able to submit solvers even at earlier stages by specifying that their submission is meant to be used for QBFEVAL'08. Registration to the web portal will enable the participants to submit their solvers, to download a pool of instances having a certified satisfiability result, and, later, to view the results while the evaluation is running. Shortly after the registration, you will receive an automatically generated acknowledgement message containing a login, a password, and the instructions to log into the QBFLIB/QBFEVAL portal. You can use your account to upload your 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. You will receive a message with a log of the process, confirming a successfull 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 you can provide us with a compiled ELF-32 executable for Linux (statically linked). The requirements for the solvers are the following: * 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). * The solver must take exactly one command line input, i.e., the file containing the QBF instance to be processed. * The solver must run as a single process (or a batch of processes). * The solver must not enforce any internal time limitation (time out and time measuring will be controlled by the evaluation scripts). * The solver must read instances using the QDIMACS 1.1 input format or the QBF 1.0 non-prenex, non-cnf format. * The solver must exit upon completion using exit code 10, if the instance is satisfiabile, or exit code 20, if the instance is unsatisfiable (any other exit code is interpreted as "the instance could not be solved"). * Finally, the solver can output additional information and a partial certificate of truth/falsity on standard output according to QDIMACS 1.1 output format or the QBF 1.0 output 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. All the authors of the solvers complying to the QDIMACS standard, will receive a pool of certified instances to be used for self-validation purposes. In the event of problems on such instances, the authors are encouraged to fix any bugs before the submission deadline. 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). QBF instances submission Authors of the instances/generators will be required to register to the QBFLIB/QBFEVAL web portal (www.qbflib.org) no later than January 15, 2008. Registered users of QBFLIB will be able to submit instances even at earlier stages by specifying that their submission is meant to be used for QBFEVAL'08. Registration to the web portal will enable unregistered participants to submit their instances, later, to view the results while the evaluation is running. Shortly after the registration, you will receive an automatically generated acknowledgement message containing a login, a password, and the instructions to log into the QBFLIB/QBFEVAL portal. You can use your account to upload your instances. The instances will be (automatically) checked for compliance with the requirements for the evaluation. You will receive a message with a log of the process, confirming a successfull submission or prompting for problems. The requirements for the QBF instances in QDIMACS are the following: * the instance must have the extension ".qdimacs.gz" indicating a text file in QDIMACS format compressed with the utility program gzip; * the instance must be formatted according to the QDIMACS 1.1 input format (this includes the instances produced by generators). The requirements for the QBF instances in non-prenex, non-cnf format are the following: * the instance must have the extension ".qbf.gz" indicating a text file in QBF 1.0 non-prenex, non-cnf format compressed with the utility program gzip; * the instance must be formatted according to the QBF 1.0 format (this includes the instances produced by generators). A QDIMACS to QBF 1.0 format (and vice versa) converter will be available shortly. Please notice that the instances submitted to the evaluation will be automatically made available for download on the QBFLIB portal. Therefore, by completing the submission to QBFEVAL the authors implicitely grant permission to the maintainers of QBFLIB to store and redistribute their work. If you cannot comply to this policy, please contact the organizers at qbf08@qbflib.org to explore alternative possibilities. QBFEVAL'08 rules Hardware and Software The competition will run on a cluster of 10 identical PCs, equipped with: * Intel Core 2 Duo 2.13Ghz processors * 4GB of RAM * Ubuntu/GNU Linux (7.04 version) operating system Test set The test set of QBFEVAL'08 will be a selection of fixed structure formulas (FSFs) that includes the following ones: * Formulas with hardness degree[1] higher than 0.3 considering all past QBFEVAL results. * All hard formulas of past evaluations. This pool is downloadable clicking here. * Formulas submitted to QBFEVAL'08 with an upper bound of 1/4 on the suites whose submitter is also authoring a competing solver. We also make available for direct download a set of certified true and false formulas. The verification of the satisfiability result was made by ChEQ. Time and memory limits We will set the CPU time limit to 600 seconds. To prevent memory swapping, we set the memory limit at 3GB. If a solver ever exceeds this bound while solving a formula, it will be considered as a memory out. Scoring rules and winner At the end of the competition, we will rank the solvers using the YASMv2[1] scoring method. References [1] Massimo Narizzano, Luca Pulina, and Armando Tacchella. Voting Systems and Automated Reasoning: the QBF Evaluation Case Study. In Proceedings of 1st International Workshop on Computational Social Choice (COMSOC) 2006. Sponsors Laboratory of Artificial Intelligence for the Diagnosis of Complex Systems www.mind-lab.it Systems and Technologies for Automated Reasoning www.star.dist.unige.it www.star-lab.it Department of Communication, Computer and System Sciences www.dist.unige.it University of Genoa www.unige.it Organization Massimo Narizzano DIST, Università di Genova Luca Pulina DIST, Università di Genova Armando Tacchella DIST, Università di Genova