(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.
Location: Lecture "Propositional satisfiability"
- Click on "Preview" to see the videos.
-No Additional Notes-
- create concept: shift + click on graph
- change concept title: shift + click on existing concept
- link together concepts: shift + click drag from one concept to another
- remove concept from graph: click on concept then press delete/backspace
- add associated content to concept: click the small circle that appears on the node when hovering over it
- other actions: use the icons in the upper right corner to optimize the graph placement, preview the graph, or download a json representation