[%%%% Apologies for multiple copies received %%%%]
[%%%% Please distribute %%%%]
CALL FOR PAPERS, SOLVERS, AND BENCHMARKS
SAT-2003
Sixth International Conference on
Theory and Applications of Satisfiability Testing
http://www.mrg.dist.unige.it/events/sat03
Co-located events:
SAT solvers competition
http://www.satlive.org/SATCompetition/
QBF solvers comparative evaluation
http://www.satlive.org/QBFEvaluation/
May 5 - 8, 2003
S. Margherita Ligure - Portofino
Italy
CONFERENCE DESCRIPTION
----------------------
The conference follows the Workshops on Satisfiability held in Siena
(1996), Paderborn (1998), and Renesse (2000), the Workshop on Theory
and Applications of Satisfiability Testing held in Boston (2001) and
in Cincinnati (2002). As in the last edition, the conference will host
a SAT solver competition, and, starting from this year, also a QBF
solvers comparative evaluation.
Great strides have been made in recent years in the theory and
practice of propositional satisfiability (SAT) testing. Even more
recently, we have seen a growing interest in the theory and practice
of quantified Boolean formulas (QBFs) satisfiability testing,
witnessed by analogous advancements both on the theoretical and on
the practical side. As a result there is growing interest in using SAT and
QBF solvers as the basis for practical tools for solving real-world
problems, as well as using the insights gained from SAT and QBF
research to create problem-specific solutions.
The purpose of this conference is to bring together researchers from
different communities -- including theoretical computer science,
artificial intelligence, verification, mathematical theorem-proving,
electrical engineering, and operations research -- in order to share
ideas and increase synergy between theoretical and empirical work.
All the aspects of propositional and QBF satisfiability testing will
be considered including, but not limited to:
- Proof Systems
- Search Techniques
- Probabilistic analysis of algorithms and their properties
- Problem encodings
- Industrial applications
- Specific tools
- Case Studies and Empirical results
Authors reporting on tools or case studies are strongly encouraged to
make the solver and/or the data publicly available on the web.
ARTICLE SUBMISSION
- ------------------
Authors should submit an extended abstract, which should not exceed 8
pages in length including tables, figures, appendices and
bibliography. Longer papers will be considered if their content
justifies it. Authors are recommended to prepare their papers by
following the Springer instructions
(http://www.springer.de/comp/lncs/authors.html).
Extended abstracts will be reviewed by at least two members of
the program committee. Inclusion of talks in the program will be
based on the results of the review process. In brief, submitted
extended abstracts must
- be in English,
- be 8 pages long at most,
- use the Springer-Verlag LNAI style
(see http://www.springer.de/comp/lncs/Authors.html),
- be submitted electronically in Postscript/PDF format.
After the conference, authors can submit a full length article.
Articles should report original research and should not exceed
16 pages in length including tables, figures, appendices and
bibliography. Full length article submissions will be rigorously
refereed and accepted articles will appear in the formal proceedings
of the Conference. It is expected that proceedings will be published
in the Lecture Notes series of Springer-Verlag. In brief, submitted
full length articles must respect the same requirements as extended
abstracts except that they must
- report original research,
- be 16 pages long at most.
Submissions deviating from these instructions may be rejected without
review. Any question regarding this policy should be directed to the
Conference Organizer prior to submission.
SOLVER AND BENCHMARK SUBMISSION
- -------------------------------
SAT solvers should be submitted in source to be compiled on a
Unix-like environment determined after submission. Machine-dependent
submissions are not possible.
The solvers are expected to read input files in the DIMACS format (see
http:://www.satlib.org/Benchmarks/SAT/satformat.ps).
For more information see the competiton web page:
http://www.satlive.org/SATCompetition/. New and challenging benchmarks
can be submitted either as a generator or as a set of instances in the
DIMACS format. Benchmarks generators and submissions composed of a
range of similar instances scaling a problem are encouraged.
QBF solvers should be submitted along the same lines of SAT
solvers. The solvers are expected to read input files in the Q-DIMACS
format (see http://www.qbflib.org/). New benchmarks can be submitted
either as a generator or as a set of instances in the Q-DIMACS format.
IMPORTANT DATES
- ---------------
SAT 2003 will be held May 5-8, 2003.
Extended abstracts submission deadline: February 8, 2003
Notification of acceptance: March 10, 2003
Final version due: April 1, 2003
SAT Solvers submission: February 14, 2003
SAT benchmarks submission: February 14, 2003
QBF Solvers submission: February 28, 2003
QBF benchmarks submission: February 28, 2003
Results of the SAT Competition: May 5-8, 2003
Results of the QBF Solvers Evaluation: May 5-8, 2003
SAT-2003 ORGANIZER
- ------------------
Enrico Giunchiglia
Universit� di Genova
[EMAIL PROTECTED]
SAT-2003 ORGANIZING COMMITTEE
- -----------------------------
Hans Kleine B�ning
Universit�t Paderborn
[EMAIL PROTECTED]
John Franco
University of Cincinnati
[EMAIL PROTECTED]
Enrico Giunchiglia
Universit� di Genova
[EMAIL PROTECTED]
Henry Kautz
University of Washington
[EMAIL PROTECTED]
Hans van Maaren
University of Delft
[EMAIL PROTECTED]
Bart Selman
Cornell University
[EMAIL PROTECTED]
Ewald Speckenmayer
Universit�t K�ln
[EMAIL PROTECTED]
SAT SOLVERS COMPETITION ORGANIZERS
- ----------------------------------
Daniel Le Berre
Universit� d'Artois
[EMAIL PROTECTED]
Laurent Simon
Universit� Paris-Sud
[EMAIL PROTECTED]
QBF SOLVERS EVALUATION ORGANIZERS
- ---------------------------------
Daniel Le Berre
Universit� d'Artois
[EMAIL PROTECTED]
Laurent Simon
Universit� Paris-Sud
[EMAIL PROTECTED]
Armando Tacchella
Universit� di Genova
[EMAIL PROTECTED]
- --
Armando Tacchella, PhD (Research scientist)
Dipartimento di Informatica Sistemistica e Telematica
Viale Causa, 15
16145 Genova
Tel. +39-010-3532782 e-mail [EMAIL PROTECTED]
Fax. +39-010-3532948 url www.mrg.dist.unige.it/~tac
