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

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

Все союзы литералов и все дизъюнкции литералов находятся в CNF, поскольку их можно рассматривать как союзы однобуквенных предложений и союзов одного предложения, соответственно. Как и в дизъюнктивной нормальной форме (ДНФ), единственными пропозициональными связками, которые может содержать формула в КНФ, являются и , или , и not . Оператор not может использоваться только как часть литерала, что означает, что он может предшествовать только пропозициональной переменной или символу предиката .

В автоматическом доказательстве теорем понятие « нормальная форма клаузии » часто используется в более узком смысле, имея в виду конкретное представление формулы CNF в виде набора наборов литералов.

Примеры и не примеры [ править ]

Все следующие формулы в переменных A, B, C, D, E и F находятся в конъюнктивной нормальной форме:

• ${\displaystyle (A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F)}$
• ${\displaystyle (A\lor B)\land C}$
• ${\displaystyle A\lor B}$
• ${\displaystyle A}$

Третья формула имеет конъюнктивную нормальную форму, потому что она рассматривается как «союз» только с одним конъюнктом, а именно с предложением . Кстати, две последние формулы также находятся в дизъюнктивной нормальной форме .${\displaystyle A\lor B}$

Следующие формулы не имеют конъюнктивной нормальной формы:

• ${\displaystyle \neg (B\lor C)}$, поскольку ИЛИ вложено в НЕ
• ${\displaystyle (A\land B)\lor C}$
• ${\displaystyle A\land (B\lor (D\land E))}$, поскольку И вложено в ИЛИ

Каждую формулу можно эквивалентно записать как формулу в конъюнктивной нормальной форме. В частности, это относится к трем только что упомянутым не примерам; они соответственно эквивалентны следующим трем формулам, которые имеют конъюнктивную нормальную форму:

• ${\displaystyle \neg B\land \neg C}$
• ${\displaystyle (A\lor C)\land (B\lor C)}$
• ${\displaystyle A\land (B\lor D)\land (B\lor E).}$

Преобразование в CNF [ править ]

^[1] Каждая пропозициональная формула может быть преобразована в эквивалентную формулу в CNF. Это преобразование основано на правилах логической эквивалентности : исключении двойного отрицания , законах Де Моргана и распределительном законе .

Поскольку все пропозициональные формулы могут быть преобразованы в эквивалентные формулы в конъюнктивной нормальной форме, доказательства часто основываются на предположении, что все формулы являются КНФ. Однако в некоторых случаях это преобразование в CNF может привести к экспоненциальному взрыву формулы. Например, перевод следующей формулы, отличной от CNF, в CNF дает формулу с пунктами:${\displaystyle 2^{n}}$

${\displaystyle (X_{1}\wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \dots \vee (X_{n}\wedge Y_{n}).}$

В частности, полученная формула:

${\displaystyle (X_{1}\vee X_{2}\vee \cdots \vee X_{n})\wedge (Y_{1}\vee X_{2}\vee \cdots \vee X_{n})\wedge (X_{1}\vee Y_{2}\vee \cdots \vee X_{n})\wedge (Y_{1}\vee Y_{2}\vee \cdots \vee X_{n})\wedge \cdots \wedge (Y_{1}\vee Y_{2}\vee \cdots \vee Y_{n}).}$

Эта формула содержит пункты; каждое предложение содержит одно или для каждого .${\displaystyle 2^{n}}$${\displaystyle X_{i}}$${\displaystyle Y_{i}}$${\displaystyle i}$

Существуют преобразования в CNF, которые избегают экспоненциального увеличения размера, сохраняя выполнимость, а не эквивалентность . ^{[2] [3]} Эти преобразования гарантируют только линейное увеличение размера формулы, но вводят новые переменные. Например, приведенная выше формула может быть преобразована в CNF путем добавления следующих переменных :${\displaystyle Z_{1},\ldots ,Z_{n}}$

${\displaystyle (Z_{1}\vee \cdots \vee Z_{n})\wedge (\neg Z_{1}\vee X_{1})\wedge (\neg Z_{1}\vee Y_{1})\wedge \cdots \wedge (\neg Z_{n}\vee X_{n})\wedge (\neg Z_{n}\vee Y_{n}).}$

Интерпретация удовлетворяет эта формула только тогда , когда по крайней мере один из новых переменных верно. Если эта переменная есть , то оба и также верны. Это означает, что каждая модель , удовлетворяющая этой формуле, также удовлетворяет исходной. С другой стороны, только некоторые из моделей исходной формулы удовлетворяют этой модели: поскольку они не упоминаются в исходной формуле, их значения не имеют отношения к ее удовлетворению, чего нет в последней формуле. Это означает, что исходная формула и результат перевода равнозначны, но не эквивалентны .${\displaystyle Z_{i}}$${\displaystyle X_{i}}$${\displaystyle Y_{i}}$${\displaystyle Z_{i}}$

Альтернативный перевод, преобразование Цейтина , также включает в себя клаузулы . С этими пунктами формула подразумевает ; эта формула часто рассматривается как «определение» как название для .${\displaystyle Z_{i}\vee \neg X_{i}\vee \neg Y_{i}}$${\displaystyle Z_{i}\equiv X_{i}\wedge Y_{i}}$${\displaystyle Z_{i}}$${\displaystyle X_{i}\wedge Y_{i}}$

Логика первого порядка [ править ]

В логике первого порядка конъюнктивная нормальная форма может быть взята дальше, чтобы получить клаузальную нормальную форму логической формулы, которую затем можно использовать для выполнения разрешения первого порядка . В автоматическом доказательстве теорем на основе разрешающей способности формула CNF

${\displaystyle (}$

${\displaystyle l_{11}}$

${\displaystyle \lor }$

${\displaystyle \ldots }$

${\displaystyle \lor }$

${\displaystyle l_{1n_{1}}}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \ldots }$

${\displaystyle \land }$

${\displaystyle (}$

${\displaystyle l_{m1}}$

${\displaystyle \lor }$

${\displaystyle \ldots }$

${\displaystyle \lor }$

${\displaystyle l_{mn_{m}}}$

${\displaystyle )}$

, с литералами, обычно представляется как набор наборов${\displaystyle l_{ij}}$

${\displaystyle \{}$

${\displaystyle \{}$

${\displaystyle l_{11}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle l_{1n_{1}}}$

${\displaystyle \}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle \{}$

${\displaystyle l_{m1}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle l_{mn_{m}}}$

${\displaystyle \}}$

${\displaystyle \}}$

.

См ниже в качестве примера.

Вычислительная сложность [ править ]

Важный набор проблем вычислительной сложности включает нахождение присвоений переменным булевой формулы, выраженной в конъюнктивной нормальной форме, таким образом, чтобы формула была истинной. Задача k -SAT - это проблема нахождения удовлетворительного присваивания булевой формуле, выраженной в CNF, в которой каждая дизъюнкция содержит не более k переменных. 3-SAT является NP-полной (как и любая другая задача k -SAT с k > 2), в то время как 2-SAT, как известно, имеет решения за полиномиальное время . Как следствие, ^[4] задача преобразования формулы в ДНФ, сохраняя выполнимость, NP-трудна ; в общем , преобразование в CNF с сохранением достоверности также является NP-трудным; следовательно, преобразование с сохранением эквивалентности в DNF или CNF снова является NP-трудным.

Типичные проблемы в этом случае связаны с формулами в "3CNF": конъюнктивная нормальная форма с не более чем тремя переменными на конъюнкт. Примеры таких формул, встречающихся на практике, могут быть очень большими, например, со 100 000 переменных и 1 000 000 конъюнктов.

Формула в КНФ может быть преобразована в equisatisfiable формулы в « K CNF» (для к ≥3) путем замены каждого конъюнкт с более чем K переменных двумя конъюнктов и с Z новой переменной, и повторяя так часто , как это необходимо.${\displaystyle X_{1}\vee \cdots \vee X_{k}\vee \cdots \vee X_{n}}$${\displaystyle X_{1}\vee \cdots \vee X_{k-1}\vee Z}$${\displaystyle \neg Z\vee X_{k}\cdots \vee X_{n}}$

Преобразование из логики первого порядка [ править ]

Чтобы преобразовать логику первого порядка в CNF: ^[1]

1. Преобразовать в нормальную форму отрицания .
   1. Устранение последствий и эквивалентностей: неоднократно заменять на ; заменить на . В конце концов, это устранит все вхождения и .${\displaystyle P\rightarrow Q}$${\displaystyle \lnot P\lor Q}$${\displaystyle P\leftrightarrow Q}$${\displaystyle (P\lor \lnot Q)\land (\lnot P\lor Q)}$${\displaystyle \rightarrow }$${\displaystyle \leftrightarrow }$
   2. Переместите НЕ внутрь, многократно применяя закон Де Моргана . В частности, заменить на ; заменить на ; и заменить на ; заменить на ; с . После этого a может стоять только непосредственно перед предикатным символом.${\displaystyle \lnot (P\lor Q)}$${\displaystyle (\lnot P)\land (\lnot Q)}$${\displaystyle \lnot (P\land Q)}$${\displaystyle (\lnot P)\lor (\lnot Q)}$${\displaystyle \lnot \lnot P}$${\displaystyle P}$${\displaystyle \lnot (\forall xP(x))}$${\displaystyle \exists x\lnot P(x)}$${\displaystyle \lnot (\exists xP(x))}$${\displaystyle \forall x\lnot P(x)}$${\displaystyle \lnot }$
2. Стандартизируйте переменные
   1. Для предложений, например, которые используют одно и то же имя переменной дважды, измените имя одной из переменных. Это позволяет избежать путаницы при отбрасывании кванторов. Например, переименован в .${\displaystyle (\forall xP(x))\lor (\exists xQ(x))}$${\displaystyle \forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists y\mathrm {Loves} (y,x)]}$${\displaystyle \forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists z\mathrm {Loves} (z,x)]}$
3. Сколемизируйте заявление
   1. Переместить кванторы наружу: повторно заменить на ; заменить на ; заменить на ; заменить на . Эти замены сохраняют эквивалентность, поскольку предыдущий шаг стандартизации переменных гарантировал, что этого не произойдет в . После этих замен, квантор может иметь место только в начальном префиксе формулы, но никогда не Внутри , или .${\displaystyle P\land (\forall xQ(x))}$${\displaystyle \forall x(P\land Q(x))}$${\displaystyle P\lor (\forall xQ(x))}$${\displaystyle \forall x(P\lor Q(x))}$${\displaystyle P\land (\exists xQ(x))}$${\displaystyle \exists x(P\land Q(x))}$${\displaystyle P\lor (\exists xQ(x))}$${\displaystyle \exists x(P\lor Q(x))}$${\displaystyle x}$${\displaystyle P}$${\displaystyle \lnot }$${\displaystyle \land }$${\displaystyle \lor }$
   2. Неоднократно заменяйте на , где - новый символ функции, так называемая " сколем функция ". Это единственный шаг, который сохраняет только выполнимость, а не эквивалентность. Он устраняет все экзистенциальные кванторы.${\displaystyle \forall x_{1}\ldots \forall x_{n}\;\exists y\;P(y)}$${\displaystyle \forall x_{1}\ldots \forall x_{n}\;P(f(x_{1},\ldots ,x_{n}))}$${\displaystyle f}$${\displaystyle n}$
4. Отбросьте все универсальные кванторы.
5. Распределите ИЛИ внутрь по И: несколько раз замените на .${\displaystyle P\lor (Q\land R)}$${\displaystyle (P\lor Q)\land (P\lor R)}$

Например, формула «Любой, кто любит всех животных, в свою очередь, кого-то любит» преобразуется в CNF (а затем в форму предложения в последней строке) следующим образом (выделение правила замены переиндексируется в ):${\displaystyle {\color {red}{\text{red}}}}$

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \forall y}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \color {red}\rightarrow }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \rightarrow }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \forall y}$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\rightarrow }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

на 1,1

${\displaystyle \forall x}$

${\displaystyle \color {red}\lnot }$

${\displaystyle (}$

${\displaystyle {\color {red}{\forall y}}}$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

на 1,1

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \color {red}\lnot }$

${\displaystyle (}$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

на 1,2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \color {red}\lnot }$

${\displaystyle \color {red}\lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

на 1,2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \color {red}\exists }$

${\displaystyle \color {red}y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

на 1,2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle (}$

${\displaystyle \color {red}\exists }$

${\displaystyle \color {red}z}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle z}$

${\displaystyle ,x)}$

${\displaystyle )}$

на 2

${\displaystyle \forall x}$

${\displaystyle \exists z}$

${\displaystyle (}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle z}$

${\displaystyle ,x)}$

на 3,1

${\displaystyle \forall x}$

${\displaystyle {\color {red}{\exists z}}}$

${\displaystyle \exists y}$

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle z}$

${\displaystyle ,x)}$

на 3,1

${\displaystyle \forall x}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

на 3,2

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle \color {red}\land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

по 4

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

${\displaystyle )}$

${\displaystyle \color {red}\land }$

${\displaystyle (}$

${\displaystyle \lnot \mathrm {Loves} (x,f(x))}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (g(x),x)}$

${\displaystyle )}$

на 5

${\displaystyle \{}$

${\displaystyle \{}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle ,}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

${\displaystyle \}}$

${\displaystyle ,}$

${\displaystyle \{}$

${\displaystyle \lnot \mathrm {Loves} (x,f(x))}$

${\displaystyle ,}$

${\displaystyle \mathrm {Loves} (g(x),x)}$

${\displaystyle \}}$

${\displaystyle \}}$

( представление статьи )

Неформально, функция skolem может рассматриваться как уступка человеку, которого любит, в то время как рождение животного (если оно есть), которое не любит. Третья последняя строка снизу читается как « не любит животное , иначе его любят » .${\displaystyle g(x)}$${\displaystyle x}$${\displaystyle f(x)}$${\displaystyle x}$${\displaystyle x}$${\displaystyle f(x)}$${\displaystyle x}$${\displaystyle g(x)}$

Вторая последняя строка сверху - это CNF.${\displaystyle (\mathrm {Animal} (f(x))\lor \mathrm {Loves} (g(x),x))\land (\lnot \mathrm {Loves} (x,f(x))\lor \mathrm {Loves} (g(x),x))}$

Заметки [ править ]

См. Также [ править ]

• Алгебраическая нормальная форма
• Дизъюнктивная нормальная форма
• Оговорка о роге
• Алгоритм Куайна – Маккласки

Ссылки [ править ]

• Дж. Элдон Уайтситт (24 мая 2012 г.). Булева алгебра и ее приложения . Курьерская корпорация. ISBN 978-0-486-15816-7.
• Ханс Кляйне Бюнинг; Теодор Леттманн (28 августа 1999 г.). Логика высказываний: дедукция и алгоритмы . Издательство Кембриджского университета. ISBN 978-0-521-63017-7.
• Пол Джексон, Дэниел Шеридан: Преобразования форм предложения для логических схем . В: Holger H. Hoos, David G. Mitchell (Eds.): Theory and Applications of Satisfiability Testing, 7-я Международная конференция, SAT 2004, Ванкувер, Британская Колумбия, Канада, 10–13 мая 2004 г., Пересмотренные избранные статьи. Конспект лекций по информатике 3542, Springer 2005, стр. 183–198
• Г. С. Цейтин: О сложности вывода в исчислении высказываний . В кн .: Слисенко А.О. (ред.) Структуры в конструктивной математике и математической логике, часть II, Семинары по математике, с. 115–125. Математический институт им. В. А. Стеклова (1968)

Внешние ссылки [ править ]

• "Конъюнктивная нормальная форма" , Энциклопедия математики , EMS Press , 2001 [1994]
• Java-апплет для преобразования в CNF и DNF, показывающий используемые законы