[We apologize if you receive multiple copies of this call] ----------------------- CALL FOR CONTRIBUTIONS QBF Gallery http://www.kr.tuwien.ac.at/events/qbfgallery2013/ Event affiliated with SAT 2013 conference and QBF 2013 workshop July 8 - 12, 2013 Helsinki, Finland SAT 2013: http://sat2013.cs.helsinki.fi/ QBF 2013: http://fmv.jku.at/qbf2013/ ----------------------- The Quantified Boolean Formulas (QBF) Gallery offers a comparative environment to evaluate QBF solvers and related tools on selected benchmarks. QBF researchers and users are invited to contribute their solvers, tools, and benchmarks to be used for evaluation. The goal of the QBF Gallery is to empirically assess the state of the art in QBF solving as well as collect and select expressive benchmarks. To this end, submission of new benchmarks related to QBF applications which have been shown to be hard for QBF solvers in the past are particularly welcome. The QBF Gallery is no typical competition but has competitive aspects. There will be no prizes and no officially announced winners. Evaluation methods may be submitted as contribution, hence there may be several scoring methods used on the results. Participants will have the opportunity to actively take part in the selection of benchmarks and evaluation runs in a discussion group (further details will be sent to the participants after registration; see below). The actual schedule of evaluation runs and the benchmarks selection depend on the number and types of submitted systems and on available computational resources. The evaluation runs of the QBF Gallery will be performed in an iterative manner, i.e., the results will be provided to the participants as soon as they are available, allowing for community-driven feedback rounds. We hereby invite submission of various kinds of tools (e.g., solvers, preprocessors, certification tools) and benchmarks (e.g., application, random, generators) to the QBF Gallery. The overall exhibition of the results will be staged during the SAT 2013 conference to be held July 8 - 12 in Helsinki, Finland. ===== Types of Submissions ===== QBF Gallery is open to all kind of submissions related to evaluating and applying QBF including but not limited to: - CNF solvers - non-CNF solvers - 2QBF solvers - preprocessors - certification tools - certificate reduction tools - benchmark generators - sets of benchmark formulas - scoring and evaluation methods ===== Submission Procedure ===== Submission of contributions to the QBF Gallery consists of the following steps: 1. Starting from April 2 2013, participants send an email with subject "QBF Gallery: registration request" briefly describing the type of the planned contributions (e.g. what kind of solver, application domain of benchmarks,...) to qbf2013@easychair.org due April 15 2013. 2. Organizers will confirm registration by email and send detailed instructions regarding submission and access to discussion group. 3. Registered participants submit their contributions as instructed by the organizers due April 30 2013. IMPORTANT: submitted tools and benchmarks will not become publicly available from the organizers (neither to the other participants). Linux x86 (64 bit) will be the standard platform on which all tools are expected to operate. Tools may be submitted as source code or as statically linked binaries. ===== Important Dates ===== 2 April - 15 April: registration and statement of planned contribution (by email) 30 April: final submission of tools and benchmarks May, June: evaluation runs July 8-12: presentation of results during SAT 2013 conference ===== Publication ===== The results of the QBF Gallery will be published as an informal technical report available from the QBF Gallery website. A formal report is planned in the form of a paper to be submitted to ACM Journal on Experimental Algorithmics (JEA), for experiments involving tools for which source code is provided. Everyone who contributes source code and a structured brief description (along the lines of the SAT 2013 Competition) will be eligible to be an author of this version of the report. ===== Organizers ===== Florian Lonsing Vienna University of Technology, Austria Martina Seidl Johannes Kepler University Linz, Austria Allen Van Gelder University of California at Santa Cruz, USA ===== Contact ===== qbf2013@easychair.org http://www.kr.tuwien.ac.at/events/qbfgallery2013/