[SMT-LIB] QBF Gallery 2013: Call for Contributions

[Florian Lonsing]

[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 at 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 at easychair.org

http://www.kr.tuwien.ac.at/events/qbfgallery2013/