Введение

Стандартная форма булевой функции
В булевой логике дизъюнктивная нормальная форма (ДНФ) — это каноническая нормальная форма логической формулы, состоящая из дизъюнкции конъюнкций; её также можно описать как ИЛИ над И, сумму произведений или, в философской логике, как концепт кластера. Как нормальная форма, она полезна в автоматическом доказательстве теорем.

Перевод на DNF

В классической логике каждая формула высказывания может быть преобразована в ДНФ.

... синтаксическими средствами

Преобразование включает использование логических эквивалентностей, таких как устранение двойного отрицания, законы Де Моргана и дистрибутивный закон. Формулы, построенные из примитивных логических связок, могут быть преобразованы в ДНФ посредством следующей канонической системы переписывания термов:

Замечание

Предложительная формула может быть представлена ровно одним полным DNF. В отличие от этого, возможно существование нескольких обычных DNF. Например, применяя данное правило три раза, полный DNF выражения выше может быть упрощен до. Однако существуют также эквивалентные формулы DNF, которые нельзя преобразовать друг в друга с помощью этого правила, пример смотрите на рисунках.

Комплексность вычислений

Проблема булевой выполнимости для формул в конъюнктивной нормальной форме является NP-полной. По принципу двойственности, проблема опровержимости для формул в дизъюнктивной нормальной форме также является NP-полной. Следовательно, проверка того, является ли формула в ДНФ тавтологией, является co-NP-трудной задачей. И наоборот, формула в ДНФ выполнима тогда и только тогда, когда выполнима хотя бы одна из её конъюнкций. Это можно определить за полиномиальное время, просто проверив, что хотя бы одна конъюнкция не содержит противоречивых литералов.

Варианты

Важным вариантом, используемым в исследовании вычислительной сложности, является k ДНФ. Формула находится в k ДНФ, если она представлена в форме ДНФ и каждая конъюнкция содержит не более k литералов.