DIMACS Series in
Discrete Mathematics and Theoretical Computer Science

VOLUME Thirty Five
TITLE: "Satisfiability Problem: Theory and Applications"
EDITORS: Dingzhu Du, Jun Gu, and Panos M. Pardalos
Published by the American Mathematical Society

Ordering Information

This volume may be obtained from the AMS or through bookstores in your area.

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 
    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 
    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 Index of Volumes
DIMACS Homepage
Contacting the Center
Document last modified on October 28, 1998.