Definition:Boolean Satisfiability Problem
Jump to navigation
Jump to search
Problem
Let $X$ be a set of propositional variables.
Let $L$ be a set of one or more propositional formulas constructed using only:
- elements of $X$
- the $4$ unary logical connectives $\operatorname{True}$, $\operatorname{False}$, identity, and $\neg$
- the $16$ binary logical connectives.
The problem is to find truth values for all $x \in X$ such that all the formulas in $L$ are true.
Such a problem is a boolean satisfiability problem.
Example
If $L$ is the set of propositional formulas given by:
- $\neg x_1 \lor \neg x_2$
- $x_3$
- $x_3 \implies x_2$
then a solution to the boolean satisfiability problem for $L$ is:
- $x_1 = \operatorname{False}$
- $x_2 = \operatorname{True}$
- $x_3 = \operatorname{True}$
Also known as
A boolean satisfiability problem is also known as a SAT problem.
This article, or a section of it, needs explaining. In particular: What does SAT stand for? You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Explain}} from the code. |
Also see
- Cook-Levin Theorem, which proves that the boolean satisfiability problem is NP-complete.