Subject: categories: Final CFP: special issue of JAR on satisfiability

From: Toby Walsh <[email-masked]>
Date: Wed, 17 Feb 1999 15:38:30 GMT

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: [email-masked]
           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.