Нормальные формы

Как компьютер проверяет, выполнимо ли логическое условие с миллионами переменных? SAT-солверы используют CNF. Как инженер проектирует логическую схему? Он строит DNF. Нормальные формы - это «машинный код» логики.

• **SAT-солверы:** Все современные решатели логических задач работают с CNF — от верификации чипов до расписаний
• **Синтез схем:** DNF напрямую транслируется в двухуровневые логические схемы (AND-OR)
• **Оптимизация запросов:** Базы данных преобразуют WHERE-условия в нормальные формы для оптимизации

Дизъюнктивная нормальная форма

**Дизъюнктивная нормальная форма (ДНФ, DNF)** - это формула вида «дизъюнкция конъюнкций». Проще: ИЛИ из И-блоков. Каждый И-блок содержит только переменные или их отрицания.

**Терминология:** Литерал - это переменная (P) или её отрицание (¬P). Конъюнкт - это конъюнкция литералов (P ∧ ¬Q ∧ R). DNF - дизъюнкция конъюнктов.

**Как читать DNF:** Формула истинна, если хотя бы один конъюнкт истинен. Конъюнкт истинен, если все его литералы истинны. Это как чек-лист: выполни все условия ОДНОГО блока - и формула истинна.

Конъюнктивная нормальная форма

**Конъюнктивная нормальная форма (КНФ, CNF)** - это формула вида «конъюнкция дизъюнкций». Проще: И из ИЛИ-блоков. Это «зеркало» DNF: внешняя связка - ∧, внутренние - ∨.

**Терминология:** Дизъюнкт (clause) - это дизъюнкция литералов (P ∨ ¬Q ∨ R). CNF - конъюнкция дизъюнктов. Иногда дизъюнкты называют «клаузами».

**Как читать CNF:** Формула истинна, если ВСЕ дизъюнкты истинны. Дизъюнкт истинен, если хотя бы один литерал истинен. Это как список требований: нарушь хотя бы одно - и формула ложна.

Преобразование в нормальные формы

**Любая формула** пропозициональной логики может быть преобразована в DNF или CNF с помощью эквивалентных преобразований. Это гарантирует существование «канонической» формы для любого высказывания.

**Зачем нужны нормальные формы:** 1) Сравнение - две формулы эквивалентны, если их нормальные формы совпадают. 2) Алгоритмы - SAT-солверы работают с CNF. 3) Схемотехника - DNF напрямую транслируется в логические схемы.

**Дистрибутивность - ключ:** Для DNF применяем ∧ поверх ∨: A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ C). Для CNF - наоборот: ∨ поверх ∧.

Упрощение формул

**Упрощение** - это приведение формулы к более короткой эквивалентной форме. Нормальная форма не всегда минимальна - после преобразования можно применить законы поглощения и сокращения.

**Законы упрощения:** Поглощение: P ∨ (P ∧ Q) ≡ P и P ∧ (P ∨ Q) ≡ P. Сокращение: (P ∧ Q) ∨ (P ∧ ¬Q) ≡ P. Тавтология в дизъюнкте: (P ∨ ¬P ∨ Q) ≡ True.

**Карты Карно** - визуальный метод упрощения для 2-4 переменных. Группируем соседние единицы в таблице истинности и получаем минимальную DNF. Для больших формул используют алгоритм Квайна-МакКласки.

Ключевые идеи

• **DNF** — ИЛИ из И-блоков: (P ∧ Q) ∨ (¬P ∧ R). Истинна, если хотя бы один блок истинен
• **CNF** — И из ИЛИ-блоков: (P ∨ Q) ∧ (¬P ∨ R). Истинна, если все блоки истинны
• **Преобразование:** Устранить →, протолкнуть ¬ внутрь (де Морган), применить дистрибутивность
• **Упрощение:** Поглощение P ∨ (P ∧ Q) ≡ P, сокращение (P ∧ Q) ∨ (P ∧ ¬Q) ≡ P

Связанные темы

Нормальные формы - мост между теорией и практикой:

• Логическая эквивалентность — Законы эквивалентности используются для преобразования в нормальные формы
• Таблицы истинности — DNF можно построить напрямую из таблицы истинности

Вопросы для размышления

• Почему SAT-солверы используют CNF, а не DNF? (Подсказка: подумай о проверке выполнимости.)
• Для формулы с n переменными, какой максимальный размер может иметь её DNF?
• Как нормальные формы связаны с логическими вентилями AND, OR, NOT в микросхемах?

Связанные уроки

• comp-23-local-optimization
• ml-01