A formula of propositional logic is in conjunctive normal form or clausal normal form (CNF) if it is a conjunction of one or more clauses, where a clause is a disjunction of literals. It is also sometimes called product of sums and AND of ORs.
CNF enables a powerful resolution rule of inference, and this is widely used in automatic theorem proving and SAT solver.
Clause
A literals is either an atomic sentence or a negation of an atomic sentence:
A clause is a set of literals. For example:
A clause is interpreted as a disjunction of its elements. For example,
Note that the empty set