propositional satisfiability

(45 minutes to learn)

Summary

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.

Context

This concept has the prerequisites:

Goals

  • 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)

-Free-

→ Coursera: Introduction to Logic (2014)
An introductory logic course geared towards computer scientists.
Location: Lecture "Propositional satisfiability"
[external website]
Author: Michael Genesereth
Other notes:
  • Click on "Preview" to see the videos.

See also

-No Additional Notes-