Дизъюнктивная нормальная форма
англ. Disjunctive normal form
Формула логики вида «ИЛИ от кусков», где каждый кусок — конъюнкция литералов; любая булева функция приводится к ДНФ, кратчайшая ищется минимизацией.
Дизъюнктивная нормальная форма (ДНФ) — формула вида «ИЛИ от кусков», где каждый кусок — конъюнкция переменных и их отрицаний: . Внутри скобок только И, между скобками только ИЛИ, ничего глубже. Любая булева функция допускает запись в ДНФ, причём бесконечно многими способами — среди них и ищут короткую. Правила равносильных преобразований формул отрабатываются в уроке логика высказываний, системная теория функций — в булевой алгебре.
Стандартный источник ДНФ — таблица истинности: на каждой строке с единицей выписывается элементарная конъюнкция, которая «возвращает истину ровно на этом наборе», и все они соединяются дизъюнкцией. Если в каждой конъюнкции участвуют все переменные по одному разу, получается совершенная ДНФ — единственная каноническая запись. Дальше начинается экономия: склеивание и поглощение сокращают число букв, для наглядности служат карты Карно, для больших функций — алгоритм Куайна—Мак-Класки. Каждая буква в ДНФ — это вход логической схемы, а схемы любят короткие.
Частые вопросы
Чем ДНФ отличается от КНФ?
Слои перевёрнуты: в ДНФ снаружи дизъюнкция, внутри конъюнкции литералов; в конъюнктивной нормальной форме — снаружи И, внутри ИЛИ. Одна функция допускает обе формы, переход идёт через законы де Моргана и дистрибутивность. Выбор диктует задача: ДНФ естественно реализуется схемой И—ИЛИ, КНФ — ИЛИ—И, а SAT-решатели принимают формулы именно в КНФ, поэтому туда преобразуют даже теоремы.
Что такое СДНФ и зачем она нужна?
Совершенная ДНФ — вариант, где в каждой конъюнкции стоят все переменные функции: каждая либо с отрицанием, либо без. Она строится по таблице истинности механически и восстанавливается однозначно, поэтому служит канонической записью функции. Минус — объём: до слагаемых для переменных. На практике от СДНФ стартуют и сокращают поглощением, а полностью «сухую» кратчайшую форму ищут картами Карно.