coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Announcement: SAT-Race 2006

From: Carsten Sinz <carsten.sinz AT jku.at>
To: ccl AT ps.uni-sb.de, theorem-provers AT ai.mit.edu, pvs AT csl.sri.com, atp AT logic.tuwien.ac.at, nuprl AT cs.cornell.edu, cs-logic AT cs.indiana.edu, formal-methods AT cs.uidaho.edu, 4c AT 4c.ucc.ie, coq-club AT pauillac.inria.fr, qed AT mcs.anl.gov, finite-model-theory AT lists.RWTH-Aachen.DE, PetriNets AT daimi.au.dk, fm-info AT air16.larc.nasa.gov, lics AT research.bell-labs.com, logic-list AT Helsinki.FI, theory-logic AT CS.CMU.EDU, fmics AT inrialpes.fr, mailinglist AT fmeurope.org, logic-announce AT uclink4.berkeley.edu
Subject: [Coq-Club] Announcement: SAT-Race 2006
Date: Tue, 22 Nov 2005 14:11:34 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

                        [Apologies for multiple copies.]

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

***** SAT-Race 2006 *****
(http://fmv.jku.at/sat-race-2006)

August 12-15, Seattle, WA, USA
Affiliated with SAT 2006
-------------------------------------

We are pleased to announce a new competitive event for Boolean
SAT Solvers called

          SAT-Race 2006

which stands in the tradition of the SAT Competitions and will
take place before and during the SAT 2006 conference held on
August 12-15 as part of the Federated Logic Conference (FLoC)
in Seattle, WA, USA.

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 2006. 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), 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.

Details of the modus operandi are published on the web under
http://fmv.jku.at/sat-race-2006.

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

- March 31, 2006: Deadline for registering solvers.
- April-June 2006: Qualification phase; exact dates of the
  qualification rounds will be published on the web.
- June 30, 2006: Deadline for submitting final versions of the
  solvers.
- August 15, 2006: Announcement of results on the SAT 2006
  conference.

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

Chair:
    Carsten Sinz (Johannes Kepler University Linz, Austria)
Advisory Panel:
    Nina Amla (Cadence Design Systems, USA)
    Joao Marques Silva (University of Southampton, UK)
    Emmanuel Zarpas (IBM Haifa Research Lab, Israel)
Technical Consultants:
    Daniel Le Berre (Universite d'Artois, France)
    Laurent Simon (Universite Paris-Sud, France)

[Coq-Club] Announcement: SAT-Race 2006, Carsten Sinz