----------------------------------------------------------------
             Announcement / Call for Participation

                  *************************
                  ***** SAT-Race 2008 *****
                  *************************

   (http://www-sr.informatik.uni-tuebingen.de/sat-race-2008)

              May 12-15, Guangzhou, P. R. China
           Affiliated with the SAT 2008 conference.

----------------------------------------------------------------

SAT-Race 2008 is a competitive event for solvers of the Boolean
Satisfiability (SAT) problem. It is organized as a satellite event
to the Eleventh International Conference on Theory and Applications
of Satisfiability Testing (SAT'08) and stands in the tradition
of the yearly SAT Competitions that have been held since 2002
and the first SAT-Race held in 2006 in Seattle. In contrast
to the SAT Competitions, the focus of SAT-Race is on industrial
benchmarks only. Moreover, the time to solve each instance is
limited to 15 minutes.


Objective
---------

The area of SAT Solving has seen tremendous progress over the
last years. Many problems (e.g. in hardware and software
verification) that seemed to be completely out of reach a decade
ago can now be handled routinely. Besides new algorithms and
better heuristics, refined implementation techniques turned
out to be vital for this success.

To keep up the driving force in improving SAT solvers, we want
to motivate implementors to present their work to a broader
audience and to compare it with that of others.


Design and Organization
-----------------------

Researchers from both academia and industry are invited to
submit their solvers - in either source code or binary format -
to SAT-Race 2008. During SAT-Race, all entrants will have to
solve a set of benchmark instances in DIMACS CNF format that
will be drawn randomly from a pool of SAT instances. This pool
will mainly consist of benchmarks from previous SAT Competitions
(Industrial Category) and the SAT-Race 2006 pool, but may be
extended with additional instances of practical relevance.
The exact benchmark set will not be published in advance; a set
of similar benchmark instances will be made available for testing
purposes, however.

For each instance and solver there will be a time limit of 15
minutes. We will also organize qualification rounds, where
participation in at least one of them is mandatory to qualify
for the SAT-Race.

Assessment of solvers will be based on the number of
successfully handled instances and the time needed to solve
them. 

There will also be two special tracks for:
* Parallel SAT Solvers (SMP, Multi-Threaded) and
* Structural SAT Solvers taking And-Inverter-Graphs (AIGs)
  as input.

Details of the modus operandi and about the special tracks
are published on the web under
http://www-sr.informatik.uni-tuebingen.de/sat-race-2008.


Important Dates
---------------

- January 15, 2008: Deadline for registering solvers.
- February-March 2008: Qualification phase; exact dates of the
  qualification rounds will be published on the web.
- March 31, 2008: Deadline for submitting final versions of
  solvers.
- May 12-15, 2008: Announcement of results on the SAT 2008
  conference.
  

Organizing Committee
--------------------

Chair
    Carsten Sinz (Universitaet Tuebingen, Germany)
Advisory Panel
    Nina Amla (Cadence Design Systems, USA)
    Toni Jussila (OneSpin Solutions, Germany)
    Daniel Le Berre (Universite d'Artois, France)
    Panagiotis Manolios (Georgia Institute of Technology, USA)
    Lintao Zhang (Microsoft Research, USA)