Satisfiability problem

From Glossary

Jump to: navigation, search

(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.

Conjunctive normal formbutton.png

A logical expression that is written as a conjunction,

LaTeX: C_1 \wedge C_2 \wedge \ldots \wedge C_m,

where LaTeX: \wedge is the conjunction (logical and). Each LaTeX: C_i is called a clause and has the form

LaTeX: L_{i_1} \vee L_{i_2} \vee \ldots \vee L_{i_n},

where LaTeX: \vee is the disjunction (logical inclusive or) and each LaTeX: L_i is a literal -- a proposition or its negation.

Personal tools