[SMT-LIB] Call for BENCHMARKS and SOLVERS for SMT-COMP 2012
cok at frontiernet.net
cok at frontiernet.net
Mon Jan 23 17:22:10 EST 2012
======================================================================
8th International Satisfiability Modulo Theories Competition
(SMT-COMP'12)
June 30 - July 1, 2012
Manchester, UK
CALL FOR BENCHMARKS
CALL FOR ENTRANTS
======================================================================
SMT-COMP is the annual competition for Satisfiability Modulo Theories
(SMT). The goals of SMT-COMP are to spur solver advances, collect relevant
benchmarks, and encourage adoption of the SMT-LIB standard, through
friendly competition. Highlights of SMT-COMP 2012 are covered below.
The competition has been highly successful and is now in its 8th year.
For the latest information, please see the SMT-COMP web page at:
http://www.smtcomp.org/
The organizers of the competition and the SMT workshop strongly request
and encourage the submission of new benchmarks and new or improved solvers.
The event has several tracks: a main track, a parallel track, an
application track, an unsat-core track, and a proof-generation track.
Within a track there are one or more divisions, where each division
uses benchmarks from a specific SMT-LIB logic (or group of logics).
Some tracks-divisions are competitive, in that the results will be scored
and winners announced; others are exhibition, meaning that the solvers
will be evaluated and the results publicized, but no winners will be awarded.
------------------------------------------
Main changes with respect to SMT-COMP 2011
------------------------------------------
- We are concentrating on just a few of the benchmark divisions this
year for the main competition. Some divisions, such as QF_UF, are
subsumed into more expressive logics; others have received only
light interest. Our goal is to focus the competition on divisions
of particular interest to applications. All non-competition divisions
will be run in exhibition mode, if solvers are submitted against them,
and the results will be displayed and publicly reported.
As always, we encourage entrants from new research groups.
- We are retaining and accenting last year's "application track" and
encourage submission of benchmarks and competition against these
benchmarks.
- The penalty for producing an incorrect result is increased. Competitors
producing all correct results are ranked above those producing
incorrect results (a "soft" disqualification for unsound tools).
- We are adding an "unsat core" track.
- We will have an exhibition track of solvers that produce proofs.
- The competition will be run with a new StarExec service, replacing
the previous SMT-Exec service. At this writing, the new service is
still being completed and tested; it will be announced later. (The
previous service will be maintained in reserve.)
For more detailed information please refer to the rules posted at
http://www.smtcomp.org/.
In order to deliver high-quality benchmarks and to allow participants
to test their solvers we consider the deadline of April 15 strict.
Benchmarks arriving thereafter will be included in the library but
not used for SMT-COMP 2012.
--------------------------------------
Benchmarks for Main and Parallel Track
--------------------------------------
New benchmarks in all categories are welcome, particularly those
representative of applications and those relevant to this year's competition.
The potential main competition benchmark divisions for this year include the
following divisions. For detailed descriptions of the divisions, refer to the
SMT-LIB web page at http://www.smtlib.org/
* QF_BV
* QF_AUFBV
* QF_UFLIA, including benchmarks from QF_LIA
* QF_UFLRA, including benchmarks from QF_LRA
* QF_IDL
* AUFLIA+p
* AUFLIA-p
* AUFNIRA
where the benchmark categories are described below
* QF_BV (Fixed-size Bit-vectors): quantifier-free formulas over bit
vectors of fixed size.
* QF_AUFBV (Bit-vectors with Arrays and Uninterpreted Functions):
quantifier-free formulas over bit vectors of fixed size, with arrays
and uninterpreted functions and predicate symbols.
* AUFLIA+p (Linear Integer Arithmetic with Uninterpreted Functions and
Arrays, with patterns): quantified formulas to be tested for
satisfiability modulo a background theory combining linear integer
arithmetic, uninterpreted function and predicate symbols, and
extensional arrays. Benchmarks include patterns for guiding
instantiation mechanisms.
* AUFLIA-p (Linear Integer Arithmetic with Uninterpreted Functions and
Arrays, without patterns): formulas from AUFLIA+p once all patterns
have been removed.
* QF_LIA (Linear Integer Arithmetic): quantifier-free formulas to be
tested for satisfiability modulo a background theory of integer
arithmetic. The syntax of atomic formulas is restricted to contain
only linear terms.
* QF_LRA (Linear Real Arithmetic): this division is like QF_LIA,
except that the background theory is real arithmetic.
* QF_UFLIA (Linear Integer Arithmetic with Uninterpreted Functions):
this division contains benchmarks in a logic which is similar to
QF_LIA, except that it also allows uninterpreted functions and
predicates.
* QF_UFLRA (Linear Real Arithmetic with Uninterpreted Functions):
this division is similar to QF_LRA, except that it also allows
uninterpreted functions and predicates.
* QF_IDL (Integer Difference Logic): quantifier-free formulas to be
tested for satisfiability modulo a background theory of integer
arithmetic. The syntax of atomic formulas is restricted to
difference logic, i.e. x - y op c, where op is either equality or
inequality and c is an integer constant.
* AUFNIRA (Arrays, Uninterpreted Functions, and Nonlinear Arithmetic):
quantifier formulas with arrays of reals indexed by integers
(Array1), arrays of Array1 indexed by integers (Array2), and
nonlinear arithmetic over the integers and reals.
As with last year, we reserve the right to remove benchmark divisions
if we do not receive enough quality benchmarks or enough solvers in a
particular division. If you have access to benchmarks in any of these
divisions, even if they are not in the SMT-LIB format, please contact
one of the organizers (see below).
--------------------------------
Benchmarks for Application Track
--------------------------------
Benchmarks for this track exploit the incremental capabilities of
the SMT-LIB2 format, by means of which it is possible to query
the solver multiple times by adding and retracting assertions.
Each benchmark can be thought of as a "trace" dumped from the
interaction of the solver with, e.g., a model-checker. The
benchmarks will be executed using a "trace executor" which
simulates (and abstracts away) the online interaction with the
model checker.
Please refer to the rules for more details.
*** We strongly encourage submissions of benchmarks for this track. ***
We will execute the competition for any benchmark divisions for
which we have adequate benchmarks and entrants. This is expected to
include at least the divisions used in 2011: QF_BV, QF_LIA, QF_UFLIA,
and QF_LRA.
--------------------------------
Benchmarks for the unsat-core and proof-generation tracks
--------------------------------
We will develop initial benchmarks for these tracks from existing
benchmarks. However, we highly encourage submission of benchmarks
that elucidate particular problems or challenges in determining
unsatisfiable cores or generating proofs.
Note that, in SMT-LIB format, an unsat-core benchmark must have
its asserted formulae named (see the standard or contact the organizers).
The organizers are considering and accepting comment on which divisions
to use for these tracks; those divisions will be announced later.
-------
Solvers
-------
Solvers will be submitted via the StarExec service, which will be
announced later. Please refer to http://www.smtcomp.org/
for complete details on entering the competition.
---------------
Important Dates
---------------
* March 15 First version of the benchmark library for the
application track posted for comment. First version of
the benchmark scrambler, benchmark selector and trace
executor made available.
* April 15 Final version of the benchmark scrambler, benchmark
selector and trace exector made available.
* April 15 No new benchmarks can be added after this date, but
problems with existing benchmarks may be fixed.
* June 1 Benchmark libraries are frozen.
* June 15 (7pm EDT) Solvers due via StarExec (for all tracks), including
system descriptions and magic numbers for benchmark
scrambling.
* June 18 (7pm EDT) Final versions due, fixing any last-minute bugs (this
marks the end of the weekend grace period for
submissions).
* June 20 Opening value of NYSE Composite Index used to complete
random seed.
* June 26 - June 29 Dates of IJCAR main conference
* June 30 - July 1 Dates of IJCAR workshops, including the SMT workshop.
----------
Organizers
----------
Roberto Bruttomesso (University of Milan, roberto.bruttomesso at unimi.it)
David Cok - chief organizer (GrammaTech, Inc., cok at frontiernet.net)
Alberto Griggio (FBK, griggio at fbk.eu)
----------------
More Information
----------------
For details on the competition, see
http://www.smtcomp.org/
For more information on the SMT-LIB format, see
http://www.smtlib.org/
For more information about the SMT Workshop, see
http://smt2012.loria.fr/
More information about the SMT-LIB
mailing list