Call for Papers Special Issue of the Journal of Automated Reasoning SAT 2000 (satisfiability at the start of the year 2000) Guest Editors: Ian P. Gent and Toby Walsh University of Strathclyde Review Panel: Endre Boros Olivier Dubois John Franco Allen Van Gelder Henry Kautz David McAllester David Plaisted Paul Purdom Bart Selman Mark Stickel Hantao Zhang In the 1990's, there has been an explosion of research into propositional satisfiability (or SAT). There are many factors behind the increased interest in this area. One factor is the improvement of search procedures for SAT. New local search procedures like GSAT and WalkSAT are able to solve SAT problems with thousands of variables. At the same time, implementations of complete search algorithms like Davis-Putnam have been able to solve open mathematical problems. Another factor is the identification of hard SAT problems at a phase transition in solubility. A third factor is the demonstration that we can often solve real world problems by encoding them into SAT. The 1990's have also seen an improved theoretical understanding of SAT, particularly in the analysis of phase transition behaviour. In light of this, there will be a special issue of the Journal of Automated Reasoning, SAT 2000, on the state of the art for research into satisfiability as we move into the year 2000. Topics ------- We will consider empirical, theoretical or application oriented papers about SAT. Possible topics include (but are not limited to) the following: * Algorithms Complete algorithms Local search procedures Novel approaches (e.g. combinations of local and complete search, genetic algorithms and quantum computers) Learning Heuristics Implementation efficiencies * Analysis Theoretical results (e.g. average and worst case behaviour) Empirical models (e.g. heavy-tails, run-time distributions) Phase transition behaviour Approximate models of search cost * Applications Hardware verification & design Finite mathematics (e.g. quasigroup existence) Encodings (e.g. planning and scheduling) SAT benchmarks and challenges Comparisons with other areas (e.g Constraints and OR) * Extensions Non-clausal formulae Linear 0-1 constraints Quantified Boolean formulae (QSAT) Modal satisfiability Prospective contributors are warmly invited to contact either, or both, of the guest editors to discuss the suitability of topics and papers. We especially welcome papers that discuss practical applications. In addition to presenting new research, all papers should provide a brief summary of their area so that outsiders can have an overview of the state of research into SAT at the start of the new millennium. Submission ----------- Please send 3 copies of your manuscript or (preferably) a postscript file to: Dr. Ian Gent Department of Computer Science University of Strathclyde Glasgow G1 1XH Scotland E-mail: ipg@cs.strath.ac.uk Phone: +44 141 548 4527 Fax: +44 141 552 5330 Timetable ---------- To ensure topicality of the special issue, submissions, reviewing and revision of papers will be held to very fixed and tight deadlines. Submission deadline 1st March 1999 Initial reviews returned 3rd May 1999 Revised papers re-submitted 1st June 1999 Final decision 1st July 1999 LaTeX and PS files to Kluwer 1st August 1999 Publication of special issue January 2000 To help us achieve this tight timetable, we have approached eminent researchers to form a review panel, although final decisions on papers will rest with the guest editors in collaboration with the editor of JAR. We will also expect authors of submitted papers to help with reviewing to this timetable.