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
December 1996
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
Index of Volumes
DIMACS Homepage