Handbook of Satisfiability : Handbook of Satisfiability.

By: Biere, AContributor(s): Heule, M | van Maaren, H | Walsh, TMaterial type: TextTextSeries: Frontiers in Artificial Intelligence and ApplicationsPublisher: Amsterdam : IOS Press, 2009Copyright date: ©2009Description: 1 online resource (980 pages)Content type: text Media type: computer Carrier type: online resourceISBN: 9781607503767Subject(s): Algebra, Boolean -- Congresses | Computer algorithms -- Congresses | Decision making -- Congresses | Propositional calculus -- CongressesGenre/Form: Electronic books.Additional physical formats: Print version:: Handbook of Satisfiability : Handbook of SatisfiabilityDDC classification: 006.3 LOC classification: QA9.3 -- .H36 2009ebOnline resources: Click to View
Contents:
Title page -- Contents -- Part I. Theory and Algorithms -- Chapter 1. A History of Satisfiability -- 1.1 Preface: the concept of satisfiability -- 1.2 The ancients -- 1.3 The medieval period -- 1.4 The renaissance -- 1.5 The first logic machine -- 1.6 Boolean algebra -- 1.7 Frege, logicism, and quantification logic -- 1.8 Russell and Whitehead -- 1.9 G"odel's incompleteness theorem -- 1.10 Effective process and recursive functions -- 1.11 Herbrand's theorem -- 1.12 Model theory and Satisfiability -- 1.13 Completeness of first-order logic -- 1.14 Application of logic to circuits -- 1.15 Resolution -- 1.16 The complexity or resolution -- 1.17 Refinement of Resolution-Based SAT Solvers -- 1.18 Upper bounds -- 1.19 Classes of easy expressions -- 1.20 Binary Decision Diagrams -- 1.21 Probabilistic analysis: SAT algorithms -- 1.22 Probabilistic analysis: thresholds -- 1.23 Stochastic Local Search -- 1.24 Maximum Satisfiability -- 1.25 Nonlinear formulations -- 1.26 Pseudo-Boolean Forms -- 1.27 Quantified Boolean formulas -- References -- Chapter 2. CNF Encodings -- 2.1 Introduction -- 2.2 Transformation to CNF -- 2.3 Case studies -- 2.4 Desirable properties of CNF encodings -- 2.5 Conclusion -- References -- Chapter 3. Complete Algorithms -- 3.1 Introduction -- 3.2 Technical Preliminaries -- 3.3 Satisfiability by Existential Quantification -- 3.4 Satisfiability by Inference Rules -- 3.5 Satisfiability by Search: The DPLL Algorithm -- 3.6 Satisfiability by Combining Search and Inference -- 3.7 Conclusions -- References -- Chapter 4. CDCL Solvers -- 4.1 Introduction -- 4.2 Notation -- 4.3 Organization of CDCL Solvers -- 4.4 Conflict Analysis -- 4.5 Modern CDCL Solvers -- 4.6 Bibliographical and Historical Notes -- References -- Chapter 5. Look-Ahead Based SAT Solvers -- 5.1 Introduction -- 5.2 General and Historical Overview -- 5.3 Heuristics.
5.4 Additional Reasoning -- 5.5 Eager Data-Structures -- References -- Chapter 6. Incomplete Algorithms -- 6.1 Greedy Search and Focused Random Walk -- 6.2 Extensions of the Basic Local Search Method -- 6.3 Discrete Lagrangian Methods -- 6.4 The Phase Transition Phenomenon in Random k-SAT -- 6.5 A New Technique for Random k-SAT: Survey Propagation -- 6.6 Conclusion -- References -- Chapter 7. Fundaments of Branching Heuristics -- 7.1 Introduction -- 7.2 A general framework for branching algorithms -- 7.3 Branching tuples and the canonical projection -- 7.4 Estimating tree sizes -- 7.5 Axiomatising the canonical order on branching tuples -- 7.6 Alternative projections for restricted branching width -- 7.7 How to select distances and measures -- 7.8 Optimising distance functions -- 7.9 The order of branches -- 7.10 Beyond clause-sets -- 7.11 Conclusion and outlook -- References -- Chapter 8. Random Satisfiability -- 8.1 Introduction -- 8.2 The State of the Art -- 8.3 Random MAX k-SAT -- 8.4 Physical Predictions for Solution-space Geometry -- 8.5 The Role of the Second Moment Method -- 8.6 Generative models -- 8.7 Algorithms -- 8.8 Belief/Survey Propagation and the Algorithmic Barrier -- 8.9 Backtracking Algorithms -- 8.10 Exponential Running-Time for k > 3 -- References -- Chapter 9. Exploiting Runtime Variation in Complete Solvers -- 9.1 Runtime Variation in Backtrack Search -- 9.2 Exploiting Runtime Variation: Randomization and Restarts -- 9.3 Conclusion -- References -- Chapter 10. Symmetry and Satisfiability -- 10.1 Motivating Example -- 10.2 Preliminaries -- 10.3 Group Theory Basics -- 10.4 CNF Symmetry -- 10.5 Automorphism Group of a Colored Graph -- 10.6 Symmetry Detection -- 10.7 Symmetry Breaking -- 10.8 Summary and a Look Forward -- 10.9 Bibliographic Notes -- References -- Chapter 11. Minimal Unsatisfiability and Autarkies.
11.1 Introduction -- 11.2 Deficiency -- 11.3 Resolution and Homomorphism -- 11.4 Special Classes -- 11.5 Extension to non-clausal formulas -- 11.6 Minimal Falsity for QBF -- 11.7 Applications and Experimental Results -- 11.8 Generalising satisfying assignments through "autarkies -- 11.9 The autarky monoid -- 11.10 Finding and using autarkies -- 11.11 Autarky systems: Using weaker forms of autarkies -- 11.12 Connections to combinatorics -- 11.13 Generalisations and extensions of autarkies -- 11.14 Conclusion -- References -- Chapter 12. Worst-Case Upper Bounds -- 12.1 Preliminaries -- 12.2 Tractable and intractable classes -- 12.3 Upper bounds for k-SAT -- 12.4 Upper bounds for General SAT -- 12.5 How large is the exponent? -- 12.6 Summary table -- References -- Chapter 13. Fixed-Parameter Tractability -- 13.1 Introduction -- 13.2 Fixed-Parameter Algorithms -- 13.3 Parameterized SAT -- 13.4 Backdoor Sets -- 13.5 Treewidth -- 13.6 Matchings -- 13.7 Concluding Remarks -- References -- Part II. Applications and Extensions -- Chapter 14. Bounded Model Checking -- 14.1 Model Checking -- 14.2 Bounded Semantics -- 14.3 Propositional Encodings -- 14.4 Completeness -- 14.5 Induction -- 14.6 Interpolation -- 14.7 Completeness with Interpolation -- 14.8 Invariant Strengthening -- 14.9 Related Work -- 14.10 Conclusion -- References -- Chapter 15. Planning and SAT -- 15.1 Introduction -- 15.2 Notation -- 15.3 Sequential Plans -- 15.4 Parallel Plans -- 15.5 Finding a Satisfiable Formula -- 15.6 Improved SAT Solving for Planning -- 15.7 QBF and Planning with Nondeterministic Actions -- References -- Chapter 16. Software Verification -- 16.1 Programs use Bit-Vectors -- 16.2 Formal Models of Software -- 16.3 Turning Bit-Vector Arithmetic into CNF -- 16.4 Bounded Model Checking for Software -- 16.5 Predicate Abstraction using SAT -- 16.6 Conclusion -- References.
Chapter 17. Combinatorial Designs by SAT Solvers -- 17.1 Introduction -- 17.2 Quasigroup Problems -- 17.3 Ramsey and Van der Waerden Numbers -- 17.4 Covering Arrays -- 17.5 Steiner Systems -- 17.6 Mendelsohn Designs -- 17.7 Encoding Design Theory Problems -- 17.8 Conclusions and Open Problems -- References -- Chapter 18. Connections to Statistical Physics -- 18.1 Introduction -- 18.2 Phase Transitions: Basic Concepts and Illustration -- 18.3 Phase transitions in random CSPs -- 18.4 Local search algorithms -- 18.5 Decimation based algorithms -- 18.6 Conclusion -- References -- Chapter 19. MaxSAT -- 19.1 Introduction -- 19.2 Preliminaries -- 19.3 Branch and Bound Algorithms -- 19.4 Complete Inference in MaxSAT -- 19.5 Approximation Algorithms -- 19.6 Partial MaxSAT and Soft Constraints -- 19.7 Evaluations of MaxSAT Solvers -- 19.8 Conclusions -- References -- Chapter 20. Model Counting -- 20.1 Computational Complexity of Model Counting -- 20.2 Exact Model Counting -- 20.3 Approximate Model Counting -- 20.4 Conclusion -- References -- Chapter 21. Non-Clausal SAT and ATPG -- 21.1 Introduction -- 21.2 Basic Definitions -- 21.3 Satisfiability Checking for Boolean Circuits -- 21.4 Automatic Test Pattern Generation -- 21.5 Conclusions -- References -- Chapter 22. Pseudo-Boolean and Cardinality Constraints -- 22.1 Introduction -- 22.2 Basic Definitions -- 22.3 Decision Problem versus Optimization Problem -- 22.4 Expressive Power of Cardinality and Pseudo-Boolean Constraints -- 22.5 Inference Rules -- 22.6 Current Algorithms -- 22.7 Conclusion -- References -- Chapter 23. QBF Theory -- 23.1 Introduction -- 23.2 Syntax and Semantics -- 23.3 Complexity Results -- 23.4 Models and Expressive power -- 23.5 Q-Resolution -- 23.6 Quantified Horn Formulas and Q2-CNF -- References -- Chapter 24. QBFs reasoning -- 24.1 Introduction -- 24.2 Quantified Boolean Logic.
24.3 Applications of QBFs and QBF reasoning -- 24.4 QBF solvers -- 24.5 Other approaches, extensions and conclusions -- References -- Chapter 25. SAT Techniques for Modal and Description Logics -- 25.1 Introduction -- 25.2 Background -- 25.3 Basic Modal DPLL -- 25.4 Advanced Modal DPLL -- 25.5 The OBDD-based Approach -- 25.6 The Eager DPLL-based approach -- References -- Chapter 26. Satisfiability Modulo Theories -- 26.1 Introduction -- 26.2 Background -- 26.3 Eager Encodings to SAT -- 26.4 Integrating Theory Solvers into SAT Engines -- 26.5 Theory Solvers -- 26.6 Combining Theories -- 26.7 Extensions and Enhancements -- References -- Chapter 27. Stochastic Boolean Satisfiability -- 27.1 Introduction -- 27.2 Definitions and Notation -- 27.3 Complexity of SSAT and Related Problems -- 27.4 Applications -- 27.5 Analytical Results -- 27.6 Algorithms and Empirical Results -- 27.7 Stochastic Constraint Programming -- 27.8 Future Directions -- References -- Subject Index -- Cited Author Index -- Contributing Authors and Affiliations.
Summary: "Satisfiability (SAT) related topics have attracted researchers from various disciplines: logic, applied areas such as planning, scheduling, operations research and combinatorial optimization, but also theoretical issues on the theme of complexity and much more, they all are connected through SAT. My personal interest in SAT stems from actual solving: The increase in power of modern SAT solvers over the past 15 years has been phenomenal. It has become the key enabling technology in automated verification of both computer hardware and software. Bounded Model Checking (BMC) of computer hardware is now probably the most widely used model checking technique. The counterexamples that it finds are just satisfying instances of a Boolean formula obtained by unwinding to some fixed depth a sequential circuit and its specification in linear temporal logic. Extending model checking to software verification is a much more difficult problem on the frontier of current research. One promising approach for languages like C with finite word-length integers is to use the same idea as in BMC but with a decision procedure for the theory of bit-vectors instead of SAT. All decision procedures for bit-vectors that I am familiar with ultimately make use of a fast SAT solver to handle complex formulas. Decision procedures for more complicated theories, like linear real and integer arithmetic, are also used in program verification. Most of them use powerful SAT solvers in an essential way. Clearly, efficient SAT solving is a key technology for 21st century computer science. I expect this collection of papers on all theoretical and practical aspects of SAT solving will be extremely useful to both students and researchers and will lead to many further advances in the field."--Edmund Clarke (FORE Systems University Professor of Computer Science and Professor of ElectricalSummary: and Computer Engineering at Carnegie Mellon University, winner of the 2007 A.M. Turing Award).
Tags from this library: No tags from this library for this title. Log in to add tags.
    Average rating: 0.0 (0 votes)
No physical items for this record

Title page -- Contents -- Part I. Theory and Algorithms -- Chapter 1. A History of Satisfiability -- 1.1 Preface: the concept of satisfiability -- 1.2 The ancients -- 1.3 The medieval period -- 1.4 The renaissance -- 1.5 The first logic machine -- 1.6 Boolean algebra -- 1.7 Frege, logicism, and quantification logic -- 1.8 Russell and Whitehead -- 1.9 G"odel's incompleteness theorem -- 1.10 Effective process and recursive functions -- 1.11 Herbrand's theorem -- 1.12 Model theory and Satisfiability -- 1.13 Completeness of first-order logic -- 1.14 Application of logic to circuits -- 1.15 Resolution -- 1.16 The complexity or resolution -- 1.17 Refinement of Resolution-Based SAT Solvers -- 1.18 Upper bounds -- 1.19 Classes of easy expressions -- 1.20 Binary Decision Diagrams -- 1.21 Probabilistic analysis: SAT algorithms -- 1.22 Probabilistic analysis: thresholds -- 1.23 Stochastic Local Search -- 1.24 Maximum Satisfiability -- 1.25 Nonlinear formulations -- 1.26 Pseudo-Boolean Forms -- 1.27 Quantified Boolean formulas -- References -- Chapter 2. CNF Encodings -- 2.1 Introduction -- 2.2 Transformation to CNF -- 2.3 Case studies -- 2.4 Desirable properties of CNF encodings -- 2.5 Conclusion -- References -- Chapter 3. Complete Algorithms -- 3.1 Introduction -- 3.2 Technical Preliminaries -- 3.3 Satisfiability by Existential Quantification -- 3.4 Satisfiability by Inference Rules -- 3.5 Satisfiability by Search: The DPLL Algorithm -- 3.6 Satisfiability by Combining Search and Inference -- 3.7 Conclusions -- References -- Chapter 4. CDCL Solvers -- 4.1 Introduction -- 4.2 Notation -- 4.3 Organization of CDCL Solvers -- 4.4 Conflict Analysis -- 4.5 Modern CDCL Solvers -- 4.6 Bibliographical and Historical Notes -- References -- Chapter 5. Look-Ahead Based SAT Solvers -- 5.1 Introduction -- 5.2 General and Historical Overview -- 5.3 Heuristics.

5.4 Additional Reasoning -- 5.5 Eager Data-Structures -- References -- Chapter 6. Incomplete Algorithms -- 6.1 Greedy Search and Focused Random Walk -- 6.2 Extensions of the Basic Local Search Method -- 6.3 Discrete Lagrangian Methods -- 6.4 The Phase Transition Phenomenon in Random k-SAT -- 6.5 A New Technique for Random k-SAT: Survey Propagation -- 6.6 Conclusion -- References -- Chapter 7. Fundaments of Branching Heuristics -- 7.1 Introduction -- 7.2 A general framework for branching algorithms -- 7.3 Branching tuples and the canonical projection -- 7.4 Estimating tree sizes -- 7.5 Axiomatising the canonical order on branching tuples -- 7.6 Alternative projections for restricted branching width -- 7.7 How to select distances and measures -- 7.8 Optimising distance functions -- 7.9 The order of branches -- 7.10 Beyond clause-sets -- 7.11 Conclusion and outlook -- References -- Chapter 8. Random Satisfiability -- 8.1 Introduction -- 8.2 The State of the Art -- 8.3 Random MAX k-SAT -- 8.4 Physical Predictions for Solution-space Geometry -- 8.5 The Role of the Second Moment Method -- 8.6 Generative models -- 8.7 Algorithms -- 8.8 Belief/Survey Propagation and the Algorithmic Barrier -- 8.9 Backtracking Algorithms -- 8.10 Exponential Running-Time for k > 3 -- References -- Chapter 9. Exploiting Runtime Variation in Complete Solvers -- 9.1 Runtime Variation in Backtrack Search -- 9.2 Exploiting Runtime Variation: Randomization and Restarts -- 9.3 Conclusion -- References -- Chapter 10. Symmetry and Satisfiability -- 10.1 Motivating Example -- 10.2 Preliminaries -- 10.3 Group Theory Basics -- 10.4 CNF Symmetry -- 10.5 Automorphism Group of a Colored Graph -- 10.6 Symmetry Detection -- 10.7 Symmetry Breaking -- 10.8 Summary and a Look Forward -- 10.9 Bibliographic Notes -- References -- Chapter 11. Minimal Unsatisfiability and Autarkies.

11.1 Introduction -- 11.2 Deficiency -- 11.3 Resolution and Homomorphism -- 11.4 Special Classes -- 11.5 Extension to non-clausal formulas -- 11.6 Minimal Falsity for QBF -- 11.7 Applications and Experimental Results -- 11.8 Generalising satisfying assignments through "autarkies -- 11.9 The autarky monoid -- 11.10 Finding and using autarkies -- 11.11 Autarky systems: Using weaker forms of autarkies -- 11.12 Connections to combinatorics -- 11.13 Generalisations and extensions of autarkies -- 11.14 Conclusion -- References -- Chapter 12. Worst-Case Upper Bounds -- 12.1 Preliminaries -- 12.2 Tractable and intractable classes -- 12.3 Upper bounds for k-SAT -- 12.4 Upper bounds for General SAT -- 12.5 How large is the exponent? -- 12.6 Summary table -- References -- Chapter 13. Fixed-Parameter Tractability -- 13.1 Introduction -- 13.2 Fixed-Parameter Algorithms -- 13.3 Parameterized SAT -- 13.4 Backdoor Sets -- 13.5 Treewidth -- 13.6 Matchings -- 13.7 Concluding Remarks -- References -- Part II. Applications and Extensions -- Chapter 14. Bounded Model Checking -- 14.1 Model Checking -- 14.2 Bounded Semantics -- 14.3 Propositional Encodings -- 14.4 Completeness -- 14.5 Induction -- 14.6 Interpolation -- 14.7 Completeness with Interpolation -- 14.8 Invariant Strengthening -- 14.9 Related Work -- 14.10 Conclusion -- References -- Chapter 15. Planning and SAT -- 15.1 Introduction -- 15.2 Notation -- 15.3 Sequential Plans -- 15.4 Parallel Plans -- 15.5 Finding a Satisfiable Formula -- 15.6 Improved SAT Solving for Planning -- 15.7 QBF and Planning with Nondeterministic Actions -- References -- Chapter 16. Software Verification -- 16.1 Programs use Bit-Vectors -- 16.2 Formal Models of Software -- 16.3 Turning Bit-Vector Arithmetic into CNF -- 16.4 Bounded Model Checking for Software -- 16.5 Predicate Abstraction using SAT -- 16.6 Conclusion -- References.

Chapter 17. Combinatorial Designs by SAT Solvers -- 17.1 Introduction -- 17.2 Quasigroup Problems -- 17.3 Ramsey and Van der Waerden Numbers -- 17.4 Covering Arrays -- 17.5 Steiner Systems -- 17.6 Mendelsohn Designs -- 17.7 Encoding Design Theory Problems -- 17.8 Conclusions and Open Problems -- References -- Chapter 18. Connections to Statistical Physics -- 18.1 Introduction -- 18.2 Phase Transitions: Basic Concepts and Illustration -- 18.3 Phase transitions in random CSPs -- 18.4 Local search algorithms -- 18.5 Decimation based algorithms -- 18.6 Conclusion -- References -- Chapter 19. MaxSAT -- 19.1 Introduction -- 19.2 Preliminaries -- 19.3 Branch and Bound Algorithms -- 19.4 Complete Inference in MaxSAT -- 19.5 Approximation Algorithms -- 19.6 Partial MaxSAT and Soft Constraints -- 19.7 Evaluations of MaxSAT Solvers -- 19.8 Conclusions -- References -- Chapter 20. Model Counting -- 20.1 Computational Complexity of Model Counting -- 20.2 Exact Model Counting -- 20.3 Approximate Model Counting -- 20.4 Conclusion -- References -- Chapter 21. Non-Clausal SAT and ATPG -- 21.1 Introduction -- 21.2 Basic Definitions -- 21.3 Satisfiability Checking for Boolean Circuits -- 21.4 Automatic Test Pattern Generation -- 21.5 Conclusions -- References -- Chapter 22. Pseudo-Boolean and Cardinality Constraints -- 22.1 Introduction -- 22.2 Basic Definitions -- 22.3 Decision Problem versus Optimization Problem -- 22.4 Expressive Power of Cardinality and Pseudo-Boolean Constraints -- 22.5 Inference Rules -- 22.6 Current Algorithms -- 22.7 Conclusion -- References -- Chapter 23. QBF Theory -- 23.1 Introduction -- 23.2 Syntax and Semantics -- 23.3 Complexity Results -- 23.4 Models and Expressive power -- 23.5 Q-Resolution -- 23.6 Quantified Horn Formulas and Q2-CNF -- References -- Chapter 24. QBFs reasoning -- 24.1 Introduction -- 24.2 Quantified Boolean Logic.

24.3 Applications of QBFs and QBF reasoning -- 24.4 QBF solvers -- 24.5 Other approaches, extensions and conclusions -- References -- Chapter 25. SAT Techniques for Modal and Description Logics -- 25.1 Introduction -- 25.2 Background -- 25.3 Basic Modal DPLL -- 25.4 Advanced Modal DPLL -- 25.5 The OBDD-based Approach -- 25.6 The Eager DPLL-based approach -- References -- Chapter 26. Satisfiability Modulo Theories -- 26.1 Introduction -- 26.2 Background -- 26.3 Eager Encodings to SAT -- 26.4 Integrating Theory Solvers into SAT Engines -- 26.5 Theory Solvers -- 26.6 Combining Theories -- 26.7 Extensions and Enhancements -- References -- Chapter 27. Stochastic Boolean Satisfiability -- 27.1 Introduction -- 27.2 Definitions and Notation -- 27.3 Complexity of SSAT and Related Problems -- 27.4 Applications -- 27.5 Analytical Results -- 27.6 Algorithms and Empirical Results -- 27.7 Stochastic Constraint Programming -- 27.8 Future Directions -- References -- Subject Index -- Cited Author Index -- Contributing Authors and Affiliations.

"Satisfiability (SAT) related topics have attracted researchers from various disciplines: logic, applied areas such as planning, scheduling, operations research and combinatorial optimization, but also theoretical issues on the theme of complexity and much more, they all are connected through SAT. My personal interest in SAT stems from actual solving: The increase in power of modern SAT solvers over the past 15 years has been phenomenal. It has become the key enabling technology in automated verification of both computer hardware and software. Bounded Model Checking (BMC) of computer hardware is now probably the most widely used model checking technique. The counterexamples that it finds are just satisfying instances of a Boolean formula obtained by unwinding to some fixed depth a sequential circuit and its specification in linear temporal logic. Extending model checking to software verification is a much more difficult problem on the frontier of current research. One promising approach for languages like C with finite word-length integers is to use the same idea as in BMC but with a decision procedure for the theory of bit-vectors instead of SAT. All decision procedures for bit-vectors that I am familiar with ultimately make use of a fast SAT solver to handle complex formulas. Decision procedures for more complicated theories, like linear real and integer arithmetic, are also used in program verification. Most of them use powerful SAT solvers in an essential way. Clearly, efficient SAT solving is a key technology for 21st century computer science. I expect this collection of papers on all theoretical and practical aspects of SAT solving will be extremely useful to both students and researchers and will lead to many further advances in the field."--Edmund Clarke (FORE Systems University Professor of Computer Science and Professor of Electrical

and Computer Engineering at Carnegie Mellon University, winner of the 2007 A.M. Turing Award).

Description based on publisher supplied metadata and other sources.

Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2018. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries.

There are no comments on this title.

to post a comment.

Powered by Koha