Definition:Boolean Satisfiability Problem

From ProofWiki
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.




Also see