Announcement / Call for Participation

                -----  SAT-Race 2010  -----

            http://baldur.iti.uka.de/sat-race-2010

              July 11-14, Edinburgh, Scotland, UK
               Affiliated with SAT'10 / FLoC'10



SAT-Race 2010 is a competitive event for solvers of the Boolean
Satisfiability (SAT) problem. It is organized as a satellite event
to the Thirteenth International Conference on Theory and Applications
of Satisfiability Testing (SAT'10) and stands in the tradition of
the yearly SAT Competitions that have been held since 2002 and the
SAT-Races held in 2006 and 2008 in Seattle and Guangzhou. In contrast
to the SAT Competitions, the focus of SAT-Race is on application
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
2010. During SAT-Race, all entrants will have to solve a set of
benchmark instances in DIMACS CNF format (AIG format for Special
Track 2) that will be drawn randomly from a pool of instances.
This pool will mainly consist of benchmarks from previous SAT
Competitions (industrial/application category) and SAT-Races, but
may be extended with additional instances of industrial 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.

Solvers will have to qualify for SAT-Race 2010 by participating
in a qualification round.

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 available on the web under
http://baldur.iti.uka.de/sat-race-2010.


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

- April 25:    Deadline for registering solvers.
- April 30:    Deadline for submitting solvers to the qualification
               round.
- June 7:      Deadline for submitting final versions of solvers
               and solver descriptions.
- July 11-14:  Announcement of results on the SAT'10 conference.
  

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

Chair
    Carsten Sinz (Karlsruhe Institue of Technology, Germany)
Advisory Panel
    Aarti Gupta (NEC Labs America, USA)
    Youssef Hamadi (Microsoft Research, UK)
    Himanshu Jain (Synopsys, USA)
    Daniel Le Berre (Universite d'Artois, France)
    Panagiotis Manolios (Northeastern University, USA)
    Yakov Novikov (OneSpin Solutions, Germany)
Technical Organization
    Florian Merz (Karlsruhe Institute of Technology, Germany)