Бульдік функцияның стандартты түрі

Standard form of a boolean function
In boolean logic, a disjunctive normal form (DNF) is a canonical normal form of a logical formula consisting of a disjunction of conjunctions; it can also be described as an OR of ANDs, a sum of products, or in philosophical logic a cluster concept. As a normal form, it is useful in automated theorem proving.

In classical logic each propositional formula can be converted to DNF

The conversion involves using logical equivalences, such as double negation elimination, De Morgan's laws, and the distributive law. Formulas built from the primitive connectives can be converted to DNF by the following canonical term rewriting system:

A propositional formula can be represented by one and only one full DNF. In contrast, several plain DNFs may be possible. For example, by applying the rule three times, the full DNF of the above can be simplified to However, there are also equivalent DNF formulas that cannot be transformed one into another by this rule, see the pictures for an example.

The Boolean satisfiability problem on conjunctive normal form formulas is NP complete. By the duality principle, so is the falsifiability problem on DNF formulas. Therefore, it is co NP hard to decide if a DNF formula is a tautology. Conversely, a DNF formula is satisfiable if, and only if, one of its conjunctions is satisfiable. This can be decided in polynomial time simply by checking that at least one conjunction does not contain conflicting literals.

An important variation used in the study of computational complexity is k DNF. A formula is in k DNF if it is in DNF and each conjunction contains at most k literals.