# Satisfiability problem

### From Glossary

(SAT). Find a truth assignment to logical propositions such that a (given) collection of clauses is true (or ascertain that at least one clause must be false in every truth assignment). This fundamental problem in computational logic forms the foundation for NP-completeness. When SAT is in conjunctive normal form and may not be satisfiable, we define the problem of maximizing the number of true clauses as **MAXSAT**.

[edit]

Conjunctive normal form |

A logical expression that is written as a conjunction,

where is the conjunction (logical and). Each
is called a *clause* and has the form

where is the disjunction (logical
inclusive or) and each is a *literal* -- a
proposition or its negation.