Introduction to mathematics of satisfiability

Author(s)

• Marek, Victor W.

Bibliographic Information

Introduction to mathematics of satisfiability

Victor W. Marek

（Chapman & Hall/CRC studies in informatics series / Series editor, G.Q. Zhang）

Chapman & Hall/CRC, c2009

Note

Includes bibliographical references and index

Description and Table of Contents

Description

Although this area has a history of over 80 years, it was not until the creation of efficient SAT solvers in the mid-1990s that it became practically important, finding applications in electronic design automation, hardware and software verification, combinatorial optimization, and more. Exploring the theoretical and practical aspects of satisfiability, Introduction to Mathematics of Satisfiability focuses on the satisfiability of theories consisting of propositional logic formulas. It describes how SAT solvers and techniques are applied to problems in mathematics and computer science as well as important applications in computer engineering. The book first deals with logic fundamentals, including the syntax of propositional logic, complete sets of functors, normal forms, the Craig lemma, and compactness. It then examines clauses, their proof theory and semantics, and basic complexity issues of propositional logic. The final chapters on knowledge representation cover finite runs of Turing machines and encodings into SAT. One of the pioneers of answer set programming, the author shows how constraint satisfaction systems can be worked out by satisfiability solvers and how answer set programming can be used for knowledge representation.

Table of Contents

Preface Sets, Lattices, and Boolean Algebras Sets and Set-Theoretic Notation Posets, Lattices, and Boolean Algebras Well-Orderings and Ordinals The Fixpoint Theorem Introduction to Propositional Logic Syntax of Propositional Logic Semantics of Propositional Logic Autarkies Tautologies and Substitutions Lindenbaum Algebra Permutations Duality Semantical Consequence Normal Forms Canonical Negation-Normal Form Occurrences of Variables and Three-Valued Logic Canonical Forms Reduced Normal Forms Complete Normal Forms Lindenbaum Algebra Revisited Other Normal Forms The Craig Lemma Craig Lemma Strong Craig Lemma Tying up Loose Ends Complete Sets of Functors Beyond De Morgan Functors Tables Field Structure in Bool Incomplete Sets of Functors, Post Classes Post Criterion for Completeness If-Then-Else Functor Compactness Theorem Koenig Lemma Compactness, Denumerable Case Continuity of the Operator Cn Clausal Logic and Resolution Clausal Logic Resolution Rule Completeness Theorem Query Answering with Resolution Davis-Putnam Lemma Semantic Resolution Autark and Lean Sets Algorithms for SAT Table Method Hintikka Sets Tableaux Davis-Putnam Algorithm Boolean Constraint Propagation The DPLL Algorithm Improvements to DPLL? Reduction of the Search SAT to Decision SAT Easy Cases of SAT Positive and Negative Formulas Horn Formulas Autarkies for Horn Theories Dual Horn Formulas Krom Formulas and 2-SAT Renameable Classes of Formulas XOR Formulas SAT, Integer Programming, and Matrix Algebra Encoding of SAT as Inequalities Resolution and Other Rules of Proof Pigeon-Hole Principle and the Cutting Plane Rule Satisfiability and {-1, 1}-Integer Programming Embedding SAT into Matrix Algebra Coding Runs of Turing Machine, and "Mix-and-Match" Turing Machines The Language Coding the Runs Correctness of Our Coding Reduction to 3-Clauses Coding Formulas as Clauses and Circuits Decision Problem for Autarkies Search Problem for Autarkies Either-Or CNFs Other Cases Computational Knowledge Representation with SAT Encoding into SAT, DIMACS Format Knowledge Representation over Finite Domains Cardinality Constraints, the Language Lcc Weight Constraints Monotone Constraints Knowledge Representation and Constraint Satisfaction Extensional Relations, CWA Constraint Satisfaction and SAT Satisfiability as Constraint Satisfaction Polynomial Cases of Boolean CSP Schaefer Dichotomy Theorem Answer Set Programming Horn Logic Revisited Models of Programs Supported Models Stable Models Answer Set Programming and SAT Knowledge Representation and ASP Complexity Issues for ASP Conclusions References Index Exercises appear at the end of each chapter.

by "Nielsen BookData"

Details

• NCID: BB00317697
• ISBN:
  • 9781439801673
• Country Code: us
• Title Language Code: eng
• Text Language Code: eng
• Place of Publication: Boca Raton
• Pages/Volumes: xiii, 350 p.
• Size: 25 cm
• Classification:
  • LCC : QA9.3
  • DC22 : 511.3
• Subject Headings:
  • LCSH : Propositional calculus
  • LCSH : Logic, Symbolic and mathematical
• Parent Bibliography ID:
  • BA82250568