Introduction to Mathematics of Satisfiability
1st Edition
Published on 1. September 2009
Book
Hardback
364 pages
978-1-4398-0167-3 (ISBN)
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.
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.
Reviews / Votes
This interesting book covers the satisfiability problem with a strong focus on its mathematical background. It includes the famous theorems on the problem as well as some exotic results. ... To improve understanding, the book offers plenty of insightful examples, elegant proofs, and each chapter ends with about a dozen exercises. ... What I like most about the book is the wide variety of ideas of which the usefulness to solve many problems is almost tangible ... the book covers more potentially powerful techniques, such as the cutting plane rule and various autarky detection methods, than those used in the latest state-of-the-art solvers. ... apart from the collection of elegant proofs - from major theorems to exotic lemmas - Introduction to Mathematics of Satisfiability is also a source of inspiration for students and researchers in the field of satisfiability.-Theory and Practice of Logic Programming, Vol. 11, Issue 1
... Through very current material at the heart of the book, the author presents and analyzes general algorithms that work better than exhaustive search ... Marek also covers important special cases of the problem that turn out vulnerable to clever special attacks. ... Summing Up: Recommended.
-CHOICE, September 2010
... an invaluable reference for anyone who is interested in issues ranging from theoretical mathematical logic to computational logic. The book maintains a nice tradeoff between formalism and clarity. ... The author excels at relating his expositions to the current state of the art, and he recognizes when his discussions are only the tip of the iceberg. ... its most significant contribution is its accessible explanations of how and why algorithms and ideas expose work.
-Carlos Linares Lopez, Computing Reviews, March 2010
More details
Series
Language
English
Place of publication
Washington
United States
Target group
College/higher education
Graduate students and researchers in mathematics, computer science, and electrical engineering.
Product notice
Paper over boards
Illustrations
11 s/w Abbildungen, 18 s/w Tabellen
18 Tables, black and white; 11 Illustrations, black and white
Dimensions
Height: 235 mm
Width: 156 mm
Weight
646 gr
ISBN-13
978-1-4398-0167-3 (9781439801673)
Copyright in bibliographic data and cover images is held by Nielsen Book Services Limited or by the publishers or by their respective licensors: all rights reserved.
Schweitzer Classification
Person
Victor W. Marek is a professor in the Department of Computer Science at the University of Kentucky.
Content
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.
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.