propositional satisfiability

(45 minutes to learn)


Propositional satisfiability (SAT) is a computational problem where one is given a setence in propositional logic, and one wants to determine if there is a satisfying assignment (an assignment of truth values to all the variables which makes the assignment true). SAT is central to computer science because it is the prototypical NP-complete problem and because SAT solvers underly a lot of automated reasoning systems.


This concept has the prerequisites:


  • define the propositional satisfiability (SAT) problem
  • give a brute force algorithm in terms of truth tables
  • show that it suffices to consider inputs in conjunctive normal form
  • show how one can use satisfiability to prove a conclusion from a set of premises

Core resources (read/watch one of the following)


Coursera: Introduction to Logic (2014)
An introductory logic course geared towards computer scientists.
Author: Michael Genesereth
Other notes:
  • Click on "Preview" to see the videos.

See also

-No Additional Notes-