To order through AMS contact the AMS Customer Services Department, P.O. Box 6248, Providence, Rhode Island 02940-6248 USA. For Visa, Mastercard, Discover, and American Express orders call 1-800-321-4AMS.
You may also visit the AMS Bookstore and order directly from there. DIMACS does not distribute or sell these books.
To celebrate 25 years of research on the satisfiability (SAT) problem, a special workshop entitled ``Satisfiability Problem: Theory and Applications'' was held on March 11--13, 1996, at the DIMACS Center. The workshop was organized by Dingzhu Du, Jun Gu, and Panos Pardalos. David Johnson and Moshe Vardi involved in the early planning of the workshop. The Advisory Committee of the workshop, Bob Johnson, David Johnson, Christos Papadimitriou, Paul Purdom, and Benjamin Wah, provided suggestions and comments during this special event.
The satisfiability problem is central in the theory of computation. It is a core of computationally intractable NP-complete problems. In practice, the SAT problem is fundamental in solving many application problems in automated reasoning, computer-aided design, computer-aided manufacturing, machine vision, database, robotics, scheduling, integrated circuit design, computer architecture design, and computer networking. Methods to solve SAT problem play a crucial role in the development of efficient computing systems. There has been a strong relationship between the theory, the algorithms, and the applications of the SAT problem. This workshop brought together a group of distinguished theorists, algorithmists, and practitioners working on the SAT problem and on its industrial applications, enhancing the interaction between the three research groups.
More than 65 researchers from universities, governmental agencies, and industrial companies from ten countries around the world attended the workshop. Steve Cook, 1982 Turing Award winner, delivered a distinguished lecture on ``Finding hard instances of the satisfiability problem.'' A total of 32 invited talks were presented in the workshop. The major topics covered in the workshop included new algorithms and improved techniques for satisfiability testing, specific data structures and implementation details of the SAT algorithms, theoretical study of the SAT problem and SAT algorithms, practical and industrial SAT problems and benchmarks, and the significant case studies and practical applications of SAT problem and SAT algorithms. Overall, the workshop achieved a great success. This volume contains a collection of refereed papers from the workshop.
The workshop was sponsored by DIMACS, through grants from the National Science Foundation, the New Jersey Commission on Science and Technology, and other sources. We would like to take this opportunity to thank the sponsors, the DIMACS staff, the participants, the authors, the referees, and the American Mathematical Society, for making the workshop successful and the publication of this volume possible.
Dingzhu Du, Jun Gu, and Panos M. Pardalos
Foreword xiii Preface xv Finding hard instances of the satisfiability problem: A survey Stephen A. Cook and David G. Mitchell 1 Algorithms for the satisfiability (SAT) problem: A survey Jun Gu, Paul W. Purdom, John Franco and Benjamin W. Wah 19 Backtracking and probing Paul Walton Purdom and G. Neil Haven 153 Relative size of certain polynomial time solvable subclasses of satisfiability J. Franco 211 Complexity of hierarchicallly and 1-dimensional periodically specified problems I: Hardness results Madhav V. Marathe, Harry B. Hunt III, Richard E. Stearns and Venkatesh Radhakrishnan 225 Worst-case analyss, 3-SAT decision and lower bounds: Approaches for improved SAT algorithms Oliver Kullman 261 Satisfiability of 3CNF formulas with small clause/variable-ratio Kazuo Iwama andKazuya Takaki 315 Propositional search efficiency and first-order theorem proving David A. Plaisted and Geoffrey D. Alexander 335 Branching rules for propositional satisfiability test Jinchang Wang 351 A discrete Lagrangian-based global-search method for solving satisfiability problems Benjamin W. Wah and Yi Shang 365 Approximate solution of weighted MAX-SAT problems using GRASP M.G.C. Resende, L.S. Pitsoulis and P.M. Pardalos 393 Multispace search for satisfiability and NP-hard problems Jun Gu 407 A branch and cut algorithm for MAX-SAT and weighted MAX-SAT Steve Joy, John Mitchell and Brian Borchers 519 Surrogate constraint analysis-new heuristics and learning schemes for satisfiability problems Arne Lokketangen and Fred Glover 537 A general stochastic approach to solving problems with hard and soft constraints Henry Kautz, Bart Selman, and YueYen Jiang 573 Some fundamental properties of Boolean ring normal forms Jieh Hsiang and Guan Shieng Huang 587 The polynomial time decidability of simulation relations for finite processes: A HORNSAT based approach Sandeep K. Shukla, Daniel J. Rosenkrantz, Harry B. Hunt III and Richard E. Stearns 603 A better upper bound for the unsatisfiability threshold Lefteris M. Kirousis, Evangelous Kranakis and Danny Krizanc 643 Solving MAX-SAT with non-oblivious functions and history-based heuristics Roberto Battiti and Marco Protasi 649 On the imbalance of distributions of solutions of CNF-formulas and its impact on satisfiability solvers Ewald Speckenmeyer, Max Bohm, and Peter Heusch 669 On the use of second order derivatives for the satisfiability problem Hans Van Maaren 677 Local search for channel assignment in cellular mobile networks Craig K. Rushforth and Wei Wang 689 A GRASP clustering technique for circuit partitioning Shawki Areibi and Anthony Vannelli 711