Introduction to Mathematics of Satisfiability

Victor W. Marek is a professor in the Department of Computer Science at the University of Kentucky.

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


König 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.