Handbook of satisfiability. (English) Zbl 1183.68568

Frontiers in Artificial Intelligence and Applications 185. Amsterdam: IOS Press (ISBN 978-1-58603-929-5/hbk). xiii, 966 p. (2009).
Contents: { }
\(\mathbf{Part\ I.\ Theory\ and\ algorithms}.\)
Ch. 1: John Franco and John Martin, A history of satisfiability (3–74);
Ch. 2: Steven Prestwich, CNF encodings (75–98);
Ch. 3: Adnan Darwiche and Knot Pipatsrisawat, Complete algorithms (99–130);
Ch. 4: Joao Marques-Silva, Ines Lynce and Sharad Malik, CDCL solvers (131–154);
Ch. 5: Marijn J. H. Heule and Hans van Maaren, Look-ahead based SAT solvers (155–184);
Ch. 6: Henry Kautz, Ashish Sabharwal and Bart Selman, Incomplete algorithms (185–203);
Ch. 7: Oliver Kullmann, Fundaments of branching heuristics (205–244);
Ch. 8: Dimitris Achlioptas, Random satisfiability (245–270);
Ch. 9: Carla P. Gomes and Ashish Sabharwal, Exploiting runtime variations in complete solvers (271–288);
Ch. 10: Karem A. Sakallah, Symmetry and satisfiability (289–338);
Ch. 11: Hans Kleine Büning and Oliver Kullmann, Minimal unsatisfiability and autarkies (339–401);
Ch. 12: Evgeny Dantsin and Edward A. Hirsch, Worst-case upper bounds (403–424);
Ch. 13: Marko Samer and Stefan Szeider, Fixed-parameter tractability (425–454).
\(\mathbf{Part\ II.\ Applications\ and\ extensions}\).
Ch. 14: Armin Biere, Bounded model checking (457–481);
Ch. 15: Jussi Rintanen, Planning and SAT (483–504);
Ch. 16: Daniel Kroening, Software verification (505–532);
Ch. 17: Hantao Zhang, Combinatorial designs by SAT solvers (533–568);
Ch. 18: Fabrizio Altarelli, Rémi Monasson, Guilhem Semerjian and Francesco Zamponi, Connections to statistical physics (569–611);
Ch. 19: Chu Min Li and Felip Manyà, MaxSAT (613–631);
Ch. 20: Carla P. Gomes, Ashish Sabharwal and Bart Selman, Model counting (633–654);
Ch. 21: Rolf Drechsler, Tommi Junttila and Ilkka Niemelä, Non-clausal SAT and ATPG (655–693);
Ch. 22: Olivier Roussel and Vasco Manquinho, Pseudo-Boolean and cardinality constraints (695–733);
Ch. 23: Hans Kleine Büning and Uwe Bubeck, Theory of quantified Boolean formulas (735–760);
Ch. 24: Enrico Giunchiglia, Paolo Marin and Massimo Narizzano, Reasoning with quantified Boolean formulas (761–780);
Ch. 25: Roberto Sebastiani and Armando Tacchella, SAT techniques for modal and description logics (781–824);
Ch. 26: Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia and Cesare Tinelli, Satisfiability modulo theories (825–885);
Ch. 27: Stephen M. Majercik, Stochastic Boolean satisfiability (887–925).
Subject Index; Cited author index; Contributing authors and affiliations.
The articles of this volume will not be indexed individually.


68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68-00 General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to computer science
68T27 Logic in artificial intelligence


Full Text: Link