Специальные формы КНФ

Существует два способа представления формулы,заданной в конъюнктивной нормальной форме(КНФ,Conjunctive Normal Form,CNF),т.е имеющей вид конъюнкции выражений в скобках(clauses),каждое из которых представляет собой дизъюнкцию одного или нескольких литералов:

• КНФ в форме Крома(2-КНФ,2-Sat,2-CNF)

• КНФ в форме Хорна(Horn clause)

КНФ в форме Крома

Конъюнктивной нормальной формой(КНФ) в форме Крома - это конъюнкция выражений в скобках,каждое из которых представляет собой дизъюнкцию нескольких литералов,количество которых не превышает 2х. Эта же такая форма называется 2-CNF (2-conjunctive normal form).

Пример: [math](A \or \neg B) \and (\neg A \or C ) \and (\neg C \or B ) \cdots [/math]

В такой форме можно представить задачу 2-SAT (2-satisfiability,задача распределения значений булевым переменным таким образом, чтобы они удовлетворяли всем наложенным ограничениям).Алгоритм для решения 2-SAT может быть применим во всех задачах, где есть набор величин, каждая из которых может принимать 2 возможных значения, и есть связи между этими величинами(к примеру,такие как нахождение такого расположения меток на диаграмме, при котором никакие две не пересекаются и т.д.).

КНФ в форме Хорна

Конъюнктивной нормальной формой(КНФ) в форме Хорна - это конъюнкция выражений в скобках,каждое из которых представляет собой дизъюнкцию литералов(literal,переменная или ее отрицание),в которой присутствует не более одного неотрицательного литерала.

Пример: [math] (\neg A \or \neg B \vee \cdots \or \neg C ) \and (A \or \neg B \vee \cdots \or \neg C)[/math]

Каждая скобка состоит из,так называемых дизъюнктов Хорна.Дизъюнкт с ровно одним положительным литералом называется определенным дизъюнктом.Дизъюнкт без положительных литералов иногда называется целью или запросом(конкретно в логическом программировании).

Дизъюнкты Хорна могут быть пропозициональными формулами, либо формулами первого порядка, в зависимости от того, рассматриваются ли пропозициональные литералы(значением которых может быть логическое высказывание) или литералы первого порядка.

Пропозициональные дизъюнкты Хорна также представляют интерес для теории сложности вычислений, где задача поиска множества истинностных значений, выполняющих КНФ в форме Хорна, является P-полной.Задача выполнимости дизъюнктов Хорна первого порядка не разрешима.

Любую формулу можно представить в виде КНФ в форме Хорна.Для этого любую формулу необходимо преобразовать в КНФ(конъюнкцию элементарных дизъюнкций) и далее каждую дизъюнкцию представить в форме Хорна.

Пример:

Пусть нам дано выражение ( ¬ A v (B ^ D) ≡ B → C ) Тогда: ¬ A v (B ^ D) ≡(¬A v B) ^ (¬A v D)

B→C ≡¬B v C

(¬A v B) ^ (¬A v D) ≡ (¬B v C) - в форме Хорна.