The Satisfiability Modulo Theories Library (SMT-LIB)

[Silvio Ranise]

Dear collegue,

 we are writing you about an initiative we are promoting with the goal
of establishing a common library of benchmarks for satisfiability
problems
w.r.t. background theories.

The library (which we have called "The Satisfiability Modulo Theories
Library" or "SMT-LIB" for short) was proposed by Alessandro Armando
at the last FroCoS (see http://combination.cs.uiowa.edu/frocos/ for more

info on the FroCoS workshop series) and it will be part of the FroCoS
website.

Our expectation is that the library will be useful to people working on
decision procedures and satisfiability modulo theories in the same way
as libraries of propositional satisfiability problems have proven useful

to the SAT community.

We have set-up a mailing list

                               smt-disc at cs.uiowa.edu

(to which this email is sent) so that it will be easier for people
interested in the SMT-LIB to reach the other members.  In particular,
we think that the following two kinds of contributions are crucial for
SMT-LIB:

1) benchmarks that have been collected or produced during
    research efforts aimed at building/combining/integrating decision
    proceudures or during real verification efforts;
2) ideas and proposals to define a common format for expressing
   and presenting the benchmarks and their background theories.

(See below for a more details on these two issues and a general
discussion of the motivations and goals of SMT-LIB.)

We have also set-up the central web page and one external node
of SMT-LIB in order to give you a concrete idea of what we have in
mind. The central page lives at the following address

                      http://goedel.cs.uiowa.edu/smtlib/

and the external web page is located at

                     http://www.loria.fr/~ranise/smtlib-local/

(notice that you can reach this last also from the central page by
clicking on the link: External Nodes).

Attached below you will find a highlight of the SMT-LIB initiative. Some

of the recipients of this message (Armando, Barrett, Harrison, Ranise,
Ruess, Stump, and Tinelli) have already had an informal meeting on it
during the last FLoC. What follows reflects the discussion initiated
during that meeting.

 We are looking forward both to add external nodes and to discuss the
common format of SMT-LIB.

Best regards,


 Silvio Ranise &  Cesare Tinelli


======================================================================

-----
Goals
-----

The long term goal of the initiative is to produce a library of
benchmarks for satisfiability modulo theories. By benchmark, we mean a
set of formulae to be checked for satisfiability modulo (combination of)

background theories of interest. Examples of background theories we have

in mind are: lists, arrays (with extensionality), linear arithmetic,
etc.  Having such a library will greatly facilitate the evaluation and
the
comparison of systems for satisfiability modulo theories.


-------------
Common format
-------------

For the library to be viable and useful it should adopt a common
standard for expressing the benchmarks, and for characterizing the
background theories in a rigorous way (so that there is no doubt on
which theories are intended).
In this respect, some natural questions arise.

1) Is it sufficient to use a first-order language for the benchmarks?
   (After all, most of the research in decision procedure has
   been done in a first-order setting.)
2) If so, should we limit ourselves to ground (i.e. quantifier-free)
   satisfiability problems? Or should we also consider problems with
   quantifiers?
3) Should we use a sorted or an unsorted framework?
4) How should the background theories and their various combinations be
   defined and specified?
5) Which concrete syntax should we use for the benchmarks?

The answer to these questions is not obvious and needs some reflection
and discussion. We think that these issues should be discussed by the
various participants to this initiative (see below for an initial list),

with the goal of reaching a reasonably broad and satisfactory agreement
on how to address them. To kick-start the discussion we are going to
provide our initial proposals in a later message.


-----------------
Preliminary Phase
-----------------

Since there is a serious risk of getting bogged down in an endless
debate on how to best address the issues above, we decided to be
practical and start collecting benchmarks right away, without waiting
for every technical details to be completely ironed out.
To do that we have set up a central web site for the library
(http://combination.cs.uiowa.edu/smtlib/), which at the beginning will
provide mostly links to benckmarks locally set up by individual
contributors.

The local web pages should contain the benchmarks that each participant
is willing to share. At least initially, the benchmarks can be in the
contributor's preferred format.
In order to structure each local set of problems, we suggest to classify

them w.r.t. the background theory in which they are assumed to be
solved. For this purpose, a precise, even if not formal, description of
the background theories is required.

For example, consider the problem of checking the satisfiability of a
certain conjunction of ground literals w.r.t. some theory of arrays.  In

this case, the local web page should specify that the problem is solved
in first-order logic with equality. Then, the signature should be
specified, e.g.

    Sigma:={select/2, store/3} U {finite set of constant symbols}

(where f/n denotes the fact that the function symbol f is of arity n).
Furthermore, a description of the theory should be provided, for
instance by means of a set of axioms such as

Ax(A) :=
  {\forall A,I,E.(select(store(A,I,E),I)=E),
   \forall A,I,J,E.(\neg(I = J) ==> select(store(A,I,E),J)=select(A,J))}

(where \forall, \neg, and ==> denote the usual first-order universal
 quantifier, negation, and implication, respectively).  Finally, the
local web page should say that by theory of arrays one means the set of
all valid (first-order) logical consequences of Ax(A).


We expect that this preliminary phase---in which each partner makes his
own benchmarks available on his web site---will foster the sharing of
knowledge and give also useful hints to guide the process of
establishing a common format for the library.  For example, we expect
that a list of frequently used theories will be identified.  As a
consequence, the design of the common framework will be driven by the
needs of solving the problems arising in the specification of such
theories.


-----------
Next phases
-----------

The next step in the process will be to rigorously specify the various
background theories as well as develop a common format for the
benchmarks.
This will be followed by a translation of the benchmarks into the common

format. We envisage that this will be done by each contributor by using
whatever means he finds appropriate: by hand, by writing a translation
tool, and so on.
(We intend to seek NSF funds to support this initiative. Depending on
the amount of funds, translation tools may be developed with these funds

and then made available to the community.)
The translated benchmarks will then be stored and maintained in the
library's web site.
Finally, we envisage the possibility of publishing on the central web
site comparative results using the benchmarks in the library.


--------
Workshop
--------

As an important checkpoint in the development of the initiative, we
intend to organize a workshop on the practical aspects of decision
procedures in automated deduction.
We expect that the workshop will be held within the next CADE
conference, which will take place in Miami, Florida, from July 29 to
August 2, 2003.
The main focus of the workshop will be on the pragmatics of decision
procedures. In particular, we will solicit contributions on the
practical issues of implementing decision procedures and their
combinations, in integrating them into larger automated reasoning
systems, and (of course!) in evaluating them experimentally.  The most
important event of the workshop will be a panel discussion on the common

format and the semantical aspects of the benchmark library.  In
particular, we expect to come up with a final decision about the common
format in order to start the standardization process of the various
benchmarks.


---------
Timetable
---------

Here is a proposed time table for the library.

[aug'02] Central web page
[aug'02] Start of discussion on common format and semantics
[oct'02] Local web pages
[jan'03] NSF grant proposal submission
[jun'03] (End of) Discussion on common format and semantics
[jul'03] CADE Workshop
[???'03] Translation into common format


---------------------------------------
(Tentative) List of Participants (in no particular order)
---------------------------------------


* Alessandro Armando (U. Genova)
* Clark Barret (New York U.)
* Aaron Stump (Washington U.)
* Alessandro Cimatti (IRST-ITC)
* Roberto Sebastiani (U. of Trento)
* John Harrison (Intel)
* Deepak Kapur (U. of New Mexico)
* Silvio Ranise (INRIA)
* Harald Ruess and Natarajan Shankar (SRI)
* Greg Nelson, Jim Saxe, and Cormac Flanagan (Compaq SRC)
* Bernhard Becker (U. of Karlsruhe)
* Cesare Tinelli (U. of Iowa)
* Alan Bundy (U. of Edinburgh)
* Predrag Janicic (U. of Belgrade)
* Wolfgang Reif and Gerard Schellorn (Augsburg U.)
* Ofer Strichman and Miroslav Velev (Carnegie Mellon U.)