[%%%% 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: March 21, 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 giunchiglia@unige.it SAT-2003 ORGANIZING COMMITTEE ----------------------------- Hans Kleine Büning Universität Paderborn kbcs@upb.de John Franco University of Cincinnati franco@gauss.ececs.uc.edu Enrico Giunchiglia Università di Genova giunchiglia@unige.it Henry Kautz University of Washington kautz@cs.washington.edu Hans van Maaren University of Delft h.vanmaaren@its.tudelft.nl Bart Selman Cornell University selman@cs.cornell.edu Ewald Speckenmayer Universität Köln esp@informatik.uni-koeln.de SAT SOLVERS COMPETITION ORGANIZERS ---------------------------------- Daniel Le Berre Université d'Artois leberre@cril.univ-artois.fr Laurent Simon Université Paris-Sud laurent.simon@lri.fr QBF SOLVERS EVALUATION ORGANIZERS --------------------------------- Daniel Le Berre Université d'Artois leberre@cril.univ-artois.fr Laurent Simon Université Paris-Sud laurent.simon@lri.fr Armando Tacchella Università di Genova tac@dist.unige.it