Handbook of satisfiability. (English) Zbl 1183.68568

Biere, Armin (ed.); Heule, Marijn (ed.); van Maaren, Hans (ed.); Walsh, Toby (ed.)

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–1204);
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–402);
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–455).
\(\mathbf{Part\ II.\ Applications\ and\ extensions}\).
Ch. 14: Armin Biere, Bounded model checking (457–482);
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–612);
Ch. 19: Chu Min Li and Felip Manyà, MaxSAT (613–632);
Ch. 20: Carla P. Gomes, Ashish Sabharwaland Bart Selman, Model counting (633–654);
Ch. 21: Rolf Drechsler, Tommi Junttila and Ilkka Niemelä, Non-clausal SAT and ATPG (655–694);
Ch. 22: Olivier Roussel and Vasco Manquinho, Pseudo-Boolean and cardinality constraints (695–734);
Ch. 23: Hans Kleine Büning and Uwe Bubeck, QBF theory (735–760);
Ch. 24: Enrico Giunchiglia, Paolo Marin and Massimo Narizzano, QBFs reasoning (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 (825–886);
Ch. 27: Stephen M. Majercik, Stochastic Boolean satisfiability (887–926).
Subject Index, Cited author index, contributing authors and affiliations.
The articles of this volume will not be indexed individually.

MSC:

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

Software:

cvc3