Специальные формы КНФ — различия между версиями
(→КНФ в форме Хорна) |
(→КНФ в форме Хорна) |
||
Строка 36: | Строка 36: | ||
|statement=В данном утверждении будет приведено доказательство, предлагающее алгоритм решения. Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна можно удовлетворить. | |statement=В данном утверждении будет приведено доказательство, предлагающее алгоритм решения. Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна можно удовлетворить. | ||
|proof= | |proof= | ||
− | *'''Шаг 1.''' Найдем в данной формуле одиночно стоящие переменные. Например, для формулы <tex> x \wedge (x \vee \neg y \vee \neg z) </tex> такой переменной является <tex>x</tex>. Если такие переменные существуют, то им надо присвоить значение <tex> 1 </tex>, если переменная входит без отрицания и <tex>0</tex>, если переменная входит с отрицанием, так как в конъюнкции они должны дать <tex>1</tex>. Заметим, что если какая-либо скобка после этого обратилась в <tex> 0 </tex>, то решения не существует | + | *'''Шаг 1.''' Найдем в данной формуле одиночно стоящие переменные. Например, для формулы <tex> x \wedge (x \vee \neg y \vee \neg z) </tex> такой переменной является <tex>x</tex>. Если такие переменные существуют, то им надо присвоить значение <tex> 1 </tex>, если переменная входит без отрицания и <tex>0</tex>, если переменная входит с отрицанием, так как в конъюнкции они должны дать <tex>1</tex>. Заметим, что если какая-либо скобка после этого обратилась в <tex> 0 </tex>, то решения не существует <tex>(O(n))</tex>, где <tex> n </tex> - длина формулы. |
− | + | * Если одиночно стоящих переменных в данном выражении нет, то всем переменным надо присвоить значение <tex> 0 </tex> и булева формула разрешится. Это следует из того, что в каждом дизъюнкте есть хотя бы одна переменная с отрицанием, подставив в нее значение <tex>0</tex> мы получим <tex> 1</tex> в результате дизъюнкции. Сделав так для каждой скобки, мы получим выражение вида: <tex>1\wedge 1 \wedge ... \wedge 1</tex>, что в конечном итоге даст нам <tex> 1</tex> В таком случае дальнейшие шаги выполнять не нужно. | |
− | + | *'''Шаг 2.''' Идем по скобкам и выписываем все встречающиеся нам переменные, кроме тех, с которыми мы работали на предыдущем шаге. Если переменная входит всегда без отрицаний, то присваиваем ей значение <tex>1</tex> и <tex>0</tex>, если всегда входит с отрицаниями <tex>(O(n))</tex>. На данном шаге никакая скобка не может обратиться в <tex>0</tex>. | |
− | * Если одиночно стоящих переменных в данном выражении нет, то всем переменным надо присвоить значение <tex> 0 </tex> и булева формула разрешится. Это следует из того, что в каждом дизъюнкте есть хотя бы одна переменная с отрицанием, подставив в нее значение <tex>0</tex> мы получим <tex> 1</tex> в результате дизъюнкции. Сделав так для каждой скобки, мы получим выражение вида: <tex>1\wedge 1 \wedge ... \wedge 1</tex>, что в конечном итоге даст нам <tex> 1</tex>. | + | *'''Шаг 3.''' На данном шаге остались переменные, входящие как с отрицаниями, так и без них. Рассмотрим скобки, в которых значение всех переменных или их отрицаний уже равны <tex> 0 </tex> (это возможно только в случае, когда в скобке присутствуют одиночно стоящие переменные из первого шага, или их отрицания). Если рассматриваемая переменная входит без отрицания, то присвоим ей значение <tex> 1</tex>, иначе, присвоим ей <tex> 0 </tex> <tex> (O(n)) </tex>. Если после этого какая-либо скобка обратилось в <tex> 0 </tex>, то решения нет, иначе формула разрешима. |
}} | }} | ||
Версия 18:54, 15 июня 2016
Рассмотрим две формы, с помощью которых можно представить формулы, заданные в конъюнктивной нормальной форме, то есть имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов. Эти две формы интересны тем, что для них существует алгоритм, который может за полиномиальное время проверить, существует ли набор аргументов, на которых данная функция будет принимать значение , в то время, как для обычной функции, не представленной данной формой, эта задача является NP-полной.
Содержание
КНФ в форме Крома
Определение: |
Конъюнктивная нормальная форма (КНФ) в форме Крома (2-КНФ) (англ. 2-CNF) — это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию нескольких литералов, количество которых не превышает двух. |
Пример :
Утверждение: |
Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Крома можно удовлетворить (т.е КНФ в форме Крома не является тождественно равной ). |
Данный алгоритм подробно описан в статье о выполнимости булевых формул, заданных в форме Крома: 2SAT. |
Утверждение: |
Функцию можно задать в форме Крома выполнено следующее следствие: |
КНФ в форме Хорна
Определение: |
Конъюнктивная нормальная форма (КНФ)в форме Хорна (англ. Horn clause) — это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию литералов, в которой присутствует не более одного литерала без отрицания. |
Пример:
Каждая скобка представляет собой Дизъюнкт Хорна[1].
Любую формулу можно представить в виде КНФ в форме Хорна. Для этого формулу необходимо преобразовать в конъюнкцию элементарных дизъюнкций и далее каждую дизъюнкцию представить в форме дизьюнкта Хорна.
Утверждение: |
В данном утверждении будет приведено доказательство, предлагающее алгоритм решения. Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна можно удовлетворить. |
|
Утверждение: |
Функцию можно задать в форме Хорна выполнено следующее следствие: |