Math 2.0

Computer science Computational complexity: resources and classes Problem

Boolean satisfiability problem

Builds on Propositional logicSatisfiabilityConjunctive normal formNPP

Problem

Let x1,…,xnx_1, \dots, x_n be propositional variables. An input is a formula φ\varphi of propositional logic in the variables x1,…,xnx_1, \dots, x_n, written as a string over a finite alphabet. The Boolean satisfiability problem SAT asks whether φ\varphi is satisfiable. That is, it asks whether some assignment of the values true and false to x1,…,xnx_1, \dots, x_n makes φ\varphi true. Often the input is restricted to formulas in conjunctive normal form, a conjunction of clauses, each a disjunction of literals. For k≥1k \ge 1, the problem kk-SAT is SAT for formulas in conjunctive normal form whose clauses have at most kk literals.

Remarks

SAT lies in NP, since a satisfying assignment is a certificate that can be checked in time polynomial in the length of φ\varphi. By the Cook–Levin theorem, SAT is NP-complete, and so is 3-SAT. In contrast, 2-SAT lies in P: it reduces to finding strongly connected components of a directed graph built from the clauses. Trying all 2n2^n assignments decides SAT, and no algorithm is known that runs in polynomial time on all inputs. Modern SAT solvers, based on backtracking with clause learning, nevertheless solve many large instances from practice.

Example: (x1∨¬x2)∧(¬x1∨x2)∧(x1∨x2)(x_1 \lor \neg x_2) \land (\neg x_1 \lor x_2) \land (x_1 \lor x_2) is satisfiable, with x1x_1 and x2x_2 both true. The formula x1∧¬x1x_1 \land \neg x_1 is not satisfiable.

Reading path

To understand this page from the ground up, read these 12 pages in order. The foundations come first.

Show the path as a graph
Conjunctive normal form, concept, no evidence levelConjunctive normal fo…conceptNP, concept, no evidence levelNPconceptP, concept, no evidence levelPconceptProposition, concept, no evidence levelPropositionconceptSatisfiability, concept, no evidence levelSatisfiabilityconceptConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionPropositional logic, concept, no evidence levelPropositional logicconceptBoolean satisfiability problem, problem, no evidence levelBoolean satisfiabilit…problem
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Conjunctive normal form concept
  2. NP concept
  3. P concept
  4. Proposition concept
  5. Satisfiability concept
  6. Conjunction definition
  7. Disjunction definition
  8. Implication definition
  9. Negation definition
  10. Biconditional definition
  11. Propositional logic concept
  12. Boolean satisfiability problem problem

Where this leads

8 pages build on this one.

Further reading

  1. Web https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
About this page
Tag3QKF32ZAKN
URIm2://3QKF32ZAKN
Kindproblem
WritingW0 stub
MSC68Q17, 03B05
StatusThis copy of the site has no build data. Run m2 status 3QKF32ZAKN.
AboutSatisfiability
UsesPropositional logic, Satisfiability, Conjunctive normal form, NP, P
Same as
Changed3 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Results about this

Used by