Introduction to Mathematics of Satisfiability

Victor W. Marek

What are VitalSource eBooks?

September 22, 2009 by Chapman and Hall/CRC
Reference - 364 Pages - 11 B/W Illustrations
ISBN 9781439801741 - CAT# KE10095
Series: Chapman & Hall/CRC Studies in Informatics Series

was $104.95


SAVE ~$31.49

Add to Wish List
SAVE 25%
When you buy 2 or more print books!
See final price in shopping cart.
FREE Standard Shipping!


  • Focuses on both theoretical and practical aspects of satisfiability
  • Discusses the important topic of clausal logic
  • Reduces the satisfiability of clausal theories to classical problems of integer programming and linear algebra
  • Offers shortcuts to programming with SAT, such as a variation of predicate logic without function symbols, cardinality constraints, and monotone constraints
  • Outlines the foundations of answer set programming and how it can be used for knowledge representation
  • Explains most mathematics of SAT from first principles
  • Provides additions, corrections, and improvements to the book on the author’s website


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.

Share this Title