Специальные формы КНФ — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(→‎КНФ в форме Хорна)
Строка 1: Строка 1:
−
Существует два способа представления формулы,заданной в конъюнктивной нормальной форме(КНФ,Conjunctive Normal Form,CNF),т.е имеющей вид конъюнкции выражений в скобках(clauses),каждое из которых представляет собой дизъюнкцию одного или нескольких литералов:
+
Рассмотрим две формы, с помощью которых можно представить формулы, заданные в [[КНФ(Conjunctive Normal Form)|конъюнктивной нормальной форме]],т.е имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов:
−
 
 
−
 
−
*[[#КНФ в форме Крома|КНФ в форме Крома(2-КНФ,2-Sat,2-CNF)]]
 
−
 
 
−
*[[#КНФ в форме Хорна|КНФ в форме Хорна(Horn clause)]]
 
−
 
 
  
  
Строка 11: Строка 5:
 
{{Определение
 
{{Определение
 
|definition=
 
|definition=
−
'''Конъюнктивной нормальной формой(КНФ) в форме Крома''' - это конъюнкция выражений в скобках,каждое из которых представляет собой дизъюнкцию нескольких литералов,количество которых не превышает 2х. Эта же такая форма называется 2-CNF (2-conjunctive normal form).}}
+
'''Конъюнктивной нормальной формой(КНФ) в форме Крома''' - это конъюнкция выражений в скобках,каждое из которых представляет собой дизъюнкцию нескольких литералов,количество которых не превышает двух.}}
  
 
'''Пример:'''
 
'''Пример:'''
−
<math>(A \or \neg B) \and (\neg A \or C ) \and (\neg C \or B ) \and (\neg A \or \neg C ) \cdots </math>
 
  
−
В такой форме можно представить задачу 2-SAT (2-satisfiability,задача распределения значений булевым переменным таким образом, чтобы они удовлетворяли всем наложенным ограничениям).Алгоритм для решения 2-SAT может быть применим во всех задачах, где есть набор величин, каждая из которых может принимать 2 возможных значения, и есть связи между этими величинами.
+
<tex>(x_1\vee\overline x_2) \wedge (\overline x_1 \vee x_3 ) \wedge (\overline x_3 \vee x_2 ) \wedge (\overline x_1 \vee \overline x_2) \wedge... </tex>
 +
 
 +
 
  
 
== КНФ в форме Хорна ==
 
== КНФ в форме Хорна ==
 
{{Определение
 
{{Определение
 
|definition=
 
|definition=
−
'''Конъюнктивной нормальной формой(КНФ) в форме Хорна''' - это конъюнкция выражений в скобках,каждое из которых представляет собой дизъюнкцию литералов(literal,переменная или ее отрицание),в которой присутствует не более одного неотрицательного литерала.}}
+
'''Конъюнктивной нормальной формой(КНФ) в форме Хорна''' - это конъюнкция выражений в скобках,каждое из которых представляет собой дизъюнкцию литералов,в которой присутствует не более одного неотрицательного литерала.}}
  
 
'''Пример:'''
 
'''Пример:'''
−
<math> (\neg A \or \neg B \vee \cdots \or \neg C ) \and (A  \or \neg B  \vee \cdots \or \neg C)</math>
 
−
 
−
Каждая скобка состоит из,так называемых ''дизъюнктов Хорна''.Дизъюнкт с ровно одним положительным литералом называется ''определенным'' дизъюнктом.Дизъюнкт без положительных литералов иногда называется ''целью'' или ''запросом''(конкретно в логическом программировании).
 
  
−
Дизъюнкты Хорна могут быть пропозициональными формулами, либо формулами первого порядка, в зависимости от того, рассматриваются ли пропозициональные литералы(значением которых может быть логическое высказывание) или литералы первого порядка.
+
<tex> (\overline x_1 \vee \overline x_2 \vee ... \vee \overline x_n ) \wedge (x_1  \vee \overline x_2  \vee ... \vee \overline x_n)\wedge ...</tex>
−
 
 
−
Пропозициональные дизъюнкты Хорна также представляют интерес для теории сложности вычислений, где задача поиска множества истинностных значений, выполняющих КНФ в форме Хорна, является 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)    - в форме Хорна.
+
Каждая скобка представляет собой ''дизъюнкт Хорна''.
  
−
== См.также ==
+
Любую формулу можно представить в виде КНФ в форме Хорна.Для этого любую формулу необходимо преобразовать в конъюнкцию элементарных дизъюнкций и далее каждую дизъюнкцию представить в форме  дизьюнкта Хорна.
−
[[СКНФ]]
 

Версия 08:09, 15 октября 2010

Рассмотрим две формы, с помощью которых можно представить формулы, заданные в конъюнктивной нормальной форме,т.е имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов:


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

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


Пример:

[math](x_1\vee\overline x_2) \wedge (\overline x_1 \vee x_3 ) \wedge (\overline x_3 \vee x_2 ) \wedge (\overline x_1 \vee \overline x_2) \wedge... [/math]


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

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


Пример:

[math] (\overline x_1 \vee \overline x_2 \vee ... \vee \overline x_n ) \wedge (x_1 \vee \overline x_2 \vee ... \vee \overline x_n)\wedge ...[/math]


Каждая скобка представляет собой дизъюнкт Хорна.

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

Источник — «http://neerc.ifmo.ru/wiki/index.php?title=Специальные_формы_КНФ&oldid=4049»