boolean-logictheorem-provingsatconjunctive-normal-form

Why a Boolean Logic Statement Needs to be in Conjunctive Normal Form (CNF)


Most things I've seen on processing boolean logic formulas says first to convert it to CNF or DNF form. Wikipedia says it is "useful in automated theorem proving", but not much more.

Wondering why it is necessary to perform this step, what aspect of it is being taken advantage of in which algorithm, etc. Without knowing more, it seems that some standard algorithm would've taken advantage of this feature, then all subsequent papers would have stated it as a requirement. But perhaps it's not necessary.


Solution

  • In many fields algorithms are simpler if the input is first normalized.

    In the case of logic formulas the main issue is that they can be nested arbitrarily deeply. Hence it intuitively makes sense to flatten them and give them a regular structure.

    It turns out that transformation into clauses, especially if they are Horn clauses, is the most useful. They are what procedures like SDL resolution or DPLL work with. These are fundamental tools in logic programming, automated theorem proving, model checking, planning, etc.