Friday, March 2, 2012

[DMANET] SAT Challenge 2012 solver competition CfP

2nd Announcement / Call for Participation

----- SAT Challenge 2012 -----

http://baldur.iti.kit.edu/SAT-Challenge-2012/

Affiliated with SAT 2012,
June 17-20, Trento, Italy

************************ Revised Details *******************************

-Tracks revised:
+ Three sequential Main Tracks:
Application (SAT+UNSAT), Hard Combinatorial (SAT+UNSAT), Random (SAT)
+ Parallel Solver Track using 8 cores
+ Sequential Portfolio Track (Mixed 1/3 Application/Hard/Random)

-Rules, execution environment, and submission protocol detailed
+ Semi-automatized testing environment

-Deadlines extended
+ Solver registration and testing period begins: March 11
+ Solver registration and benchmark submission: April 2
+ Final versions of registered solver due: April 11

-Solver and benchmark descriptions booklet planned

FOR DETAILED INFORMATION:
http://baldur.iti.kit.edu/SAT-Challenge-2012/

*************************************************************************

The SAT Challenge 2012 is a competitive event for solvers for the Boolean
Satisfiability (SAT) problem. It is organized as a satellite event to the
15th International Conference on Theory and Applications of Satisfiability
Testing (SAT 2012) and stands in the tradition of the SAT Competitions
that have been held yearly from 2002 to 2005 and biannually starting from
2007, and the SAT-Races held in 2006, 2008 and 2010.

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.

THE CHALLENGE

The SAT Challenge differs from both previous SAT Competitions and
SAT-Races. Similar to SAT Competitions, there will be several tracks
suitable for different kinds of solving algorithms (e.g. complete or
local search). Similar to SAT-Races, the time to solve each instance
will be limited to 15 minutes, and the solvers' source code need not
be made publicly available (although this is strongly encouraged).

The SAT Challenge 2012 consists of five independent tracks:

* Three Main Tracks for Sequential Solvers:

- Application SAT+UNSAT:
problem encodings (both SAT and UNSAT) from real-world applications.

- Hard Combinatorial SAT+UNSAT:
hard combinatorial problems (both SAT and UNSAT) to challenge current
SAT solving algorithms.

- Random SAT:
randomly generated satisfiable instances.

* Parallel Solver Track:
Same problem instances as in the Application Main Track.
Eight cores can be used.

* Sequential Portfolio Solver Track:
1/3 mixture of application, hard combinatorial, and random instances
(both SAT and UNSAT).
A portfolio solver combines different SAT algorithms.

Complete rules of SAT Challenge 2012 are available on the challenge
web page at http://baldur.iti.kit.edu/SAT-Challenge-2012/

IMPORTANT DATES

March 11, 2012:
Solver registration and testing period begins
April 2, 2012:
Solver registration, testing, and benchmark submission deadline
April 11, 2012:
Final versions of registered solvers due

Around June 20, 2012:
Announcement of results at the SAT 2012 conference.

ORGANIZING COMMITTEE

Adrian Balint University of Ulm, Germany
Anton Belov University College Dublin, Ireland
Matti Jarvisalo University of Helsinki, Finland
Carsten Sinz Karlsruhe Institute of Technology, Germany
**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************