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

Материал из Викиконспекты
Перейти к: навигация, поиск
(КНФ в форме Крома)
(КНФ в форме Хорна)
Строка 36: Строка 36:
 
|statement= Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна можно удовлетворить.
 
|statement= Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна можно удовлетворить.
 
|proof= Далее будет приведено доказательство, предлагающее алгоритм решения.
 
|proof= Далее будет приведено доказательство, предлагающее алгоритм решения.
 +
*'''Представление функции'''
 +
 +
Функцию можно представить в любом виде. Например, можно использовать древовидную структуру. Для формулы <tex> x \wedge (x \vee \neg y \vee \neg z) </tex>, которую мы будем использовать далее, дерево может выглядеть так :
 +
[[Файл:Tree_structure.png]]
 +
 
*'''Шаг 1. Одиночное вхождение переменных'''  
 
*'''Шаг 1. Одиночное вхождение переменных'''  
  
Строка 43: Строка 48:
  
 
*'''Шаг 2.''' Идем по скобкам и выписываем все встречающиеся нам переменные, кроме тех, с которыми мы работали на предыдущем шаге. Если переменная всегда входит без отрицаний, присваиваем ей значение <tex>1</tex>, если переменная всегда входит с отрицаниями, присваиваем <tex>0</tex>. На данном шаге никакая скобка не может обратиться в <tex>0</tex>.  
 
*'''Шаг 2.''' Идем по скобкам и выписываем все встречающиеся нам переменные, кроме тех, с которыми мы работали на предыдущем шаге. Если переменная всегда входит без отрицаний, присваиваем ей значение <tex>1</tex>, если переменная всегда входит с отрицаниями, присваиваем <tex>0</tex>. На данном шаге никакая скобка не может обратиться в <tex>0</tex>.  
*'''Шаг 3.''' На данном шаге остались переменные, не являющиеся одиночно стоящими и входящие в формулу как с отрицаниями, так и без них. Рассмотрим скобки, в которых значение всех рассмотренных ранее переменных или их отрицаний уже равны <tex> 0 </tex> (это возможно только в случае, когда в скобке присутствуют одиночно стоящие переменные из первого шага, или их отрицания). Рассматриваемые на данном шаге переменные в такой скобке могут входить с отрицанием и без него. Если рассматриваемая переменная входит без отрицания, то присвоим ей значение <tex> 1 </tex>, иначе, присвоим ей <tex> 0 </tex>. Если после этого какая-либо скобка обратилась в <tex> 0 </tex>, то решения нет, иначе формула разрешима.
+
*'''Шаг 3.''' Опустим одиночно стоящие переменные и скобки, в которых значение стало равным 1, так как они уже не влияют на существование ответа. Проделаем с полученным выражением алгоритм, начиная с <tex>1</tex> шага, пока <tex>1</tex> шаг не найдёт ответ.
  
 
*Время работы алгоритма:
 
*Время работы алгоритма:
 +
Так как функция состоит из простых выражений, мы сможем её разбить на дерево за линейное время.
 
Будем считать, что длиной формулы является количество переменных, входящих в нее. Обозначим ее за <tex> n </tex>.
 
Будем считать, что длиной формулы является количество переменных, входящих в нее. Обозначим ее за <tex> n </tex>.
В каждом шаге мы проходимся по всем переменным и присваиваем некоторым из них какое-то значение. Отсюда следует, что время работы данного алгоритма линейное, относительно количества входящих переменных.
+
В каждом шаге алгоритма мы обрабатываем очередную одиночную переменную за линейное время. Отсюда следует, что время работы линейное, относительно количества входящих переменных.
 
}}
 
}}
 
{{Утверждение
 
{{Утверждение

Версия 23:46, 16 июня 2016

Рассмотрим две формы, с помощью которых можно представить формулы, заданные в конъюнктивной нормальной форме, то есть имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов. Эти две формы интересны тем, что для них существует алгоритм, который может за полиномиальное время проверить, существует ли набор аргументов, на которых данная функция будет принимать значение [math]1[/math], в то время, как для обычной функции, не представленной данной формой, эта задача является NP-полной.

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

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


Пример :

[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]

Разрешимать булевой формулы, заданой в форме Крома

Основная статья: 2SAT


Утверждение:
Функцию [math]F[/math] можно задать в форме Крома [math] \iff [/math] выполнено следующее следствие:[math] F(x_1, ..., x_n)=F(y_1, ..., y_n)=F(z_1, ..., z_n)=1 \Rightarrow[/math] [math]F(\langle x_1, y_1, z_1 \rangle, \langle x_2, y_2, z_2 \rangle, ..., \langle x_n, y_n, z_n \rangle)[/math]

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

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


Пример:

[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]

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

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

Утверждение:
Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна можно удовлетворить.
[math]\triangleright[/math]

Далее будет приведено доказательство, предлагающее алгоритм решения.

  • Представление функции

Функцию можно представить в любом виде. Например, можно использовать древовидную структуру. Для формулы [math] x \wedge (x \vee \neg y \vee \neg z) [/math], которую мы будем использовать далее, дерево может выглядеть так : Tree structure.png

  • Шаг 1. Одиночное вхождение переменных

Найдем в данной формуле одиночно стоящие переменные. Например, для формулы [math] x \wedge (x \vee \neg y \vee \neg z) [/math] такой переменной является [math]x[/math]. Присвоим всем таким переменным значение [math] 1 [/math], если переменная входит без отрицания и [math]0[/math] иначе, так как в конъюнкции они должны дать [math]1[/math]. Заметим, что если какая-либо скобка после этого обратилась в [math] 0 [/math], то решения не существует.

Если одиночно стоящих переменных в данном выражении нет, то всем переменным надо присвоить значение [math] 0 [/math] и булева формула разрешится. Это следует из того, что в каждом дизъюнкте есть хотя бы одна переменная с отрицанием, подставив в нее значение [math]0[/math] мы получим [math] 1[/math] в результате дизъюнкции.В итоге мы получим выражение вида: [math]1\wedge 1 \wedge ... \wedge 1[/math], что в результате даст нам [math] 1[/math]. В таком случае дальнейшие шаги выполнять не нужно.

  • Шаг 2. Идем по скобкам и выписываем все встречающиеся нам переменные, кроме тех, с которыми мы работали на предыдущем шаге. Если переменная всегда входит без отрицаний, присваиваем ей значение [math]1[/math], если переменная всегда входит с отрицаниями, присваиваем [math]0[/math]. На данном шаге никакая скобка не может обратиться в [math]0[/math].
  • Шаг 3. Опустим одиночно стоящие переменные и скобки, в которых значение стало равным 1, так как они уже не влияют на существование ответа. Проделаем с полученным выражением алгоритм, начиная с [math]1[/math] шага, пока [math]1[/math] шаг не найдёт ответ.
  • Время работы алгоритма:

Так как функция состоит из простых выражений, мы сможем её разбить на дерево за линейное время. Будем считать, что длиной формулы является количество переменных, входящих в нее. Обозначим ее за [math] n [/math].

В каждом шаге алгоритма мы обрабатываем очередную одиночную переменную за линейное время. Отсюда следует, что время работы линейное, относительно количества входящих переменных.
[math]\triangleleft[/math]
Утверждение:
Функцию [math]F[/math] можно задать в форме Хорна [math] \iff [/math] выполнено следующее следствие:[math] F(x_1, ..., x_n)=F(y_1, ..., y_n)=1 \Rightarrow F(x_1 \wedge y_1, x_2 \wedge y_2, ..., x_n \wedge y_n)[/math]

См.также

Примечания

Источники информации