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.
\(\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.
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 |
