You are here

Introduction to Mathematics of Satisfiability

Victor W. Marek
Publisher: 
Chapman & Hall/CRC
Publication Date: 
2009
Number of Pages: 
350
Format: 
Hardcover
Series: 
Chapman & Hall/CRC Studies in Informatics Series
Price: 
89.95
ISBN: 
9781439801673
Category: 
Monograph
We do not plan to review this book.

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