Изменения

Функцию можно представить *'''Шаг 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> 0 </tex> и булева формула разрешится. Это следует из того, что в каждом дизъюнкте есть хотя бы одна переменная с отрицанием, подставив в нее значение <tex>0</tex> мы получим <tex> 1</tex> в результате дизъюнкции. В итоге мы получим выражение вида: <tex>1\wedge 1 \wedge ... \wedge 1</tex>, что в результате даст нам <tex> 1</tex>. В таком случае дальнейшие шаги выполнять не нужно.

*'''Шаг 12. Одиночное вхождение переменных''' Найдем в данной формуле одиночно стоящие : Идем по скобкам и выписываем все встречающиеся нам переменные. Например, для формулы <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> 0 </tex> и булева формула разрешится. Это следует из того, что в каждом дизъюнкте есть хотя бы одна переменная всегда входит с отрицаниемотрицаниями, подставив в нее значение присваиваем <tex>0</tex> мы получим <tex> 1</tex> в результате дизъюнкции. В итоге мы получим выражение вида: <tex>1\wedge 1 \wedge ... \wedge 1</tex>, что На данном шаге никакая скобка не может обратиться в результате даст нам <tex> 10</tex>. В таком случае дальнейшие шаги выполнять не нужно.

*'''Шаг 23.''' Идем по скобкам :Опустим одиночно стоящие переменные и выписываем все встречающиеся нам переменныескобки, в которых значение стало равным <tex>1</tex>. По определению формы Хорна, кроме техв каждой из скобок, с которыми где мы работали на предыдущем шагеопустили переменную не больше <tex>1</tex> переменной без отрицания. Если переменная всегда входит без отрицанийЛибо какая-то из переменных внутри скобки будет иметь отрицание, присваиваем ей значение т.е. при подстановке <tex>0</tex> станет равна <tex>1</tex>, если переменная всегда входит либо мы рассмотрим переменную без отрицания как отдельно стоящую переменную. Значит <tex>1</tex> шаг алгоритма выполнится верно. Проделаем с отрицаниямиполученным выражением алгоритм, присваиваем начиная с <tex>01</tex>. На данном шаге никакая скобка не может обратиться в шага, пока <tex>01</tex>шаг не найдёт ответ.

*'''Шаг 3.''' Опустим одиночно стоящие переменные и скобки, в которых значение стало равным 1. По определению формы Хорна, в каждой из скобок, где мы опустили переменную не больше <tex>1</tex> переменной без отрицания. Либо какая-то из переменных внутри скобки будет иметь отрицание, т.е. при подстановке <tex>0</tex> станет равна <tex>1</tex>, либо мы рассмотрим переменную без отрицания как отдельно стоящую переменную. Значит <tex>1</tex> шаг алгоритма выполнится верно. Проделаем с полученным выражением алгоритм, начиная с <tex>1</tex> шага, пока <tex>1</tex> шаг не найдёт ответ. *Время работы алгоритма:Так как функция состоит из простых выражений, мы сможем её разбить на дерево за линейное время.Будем считать, что длиной формулы является количество переменных, входящих в нее. Обозначим и обозначим ее за <tex> n </tex>.В каждом шаге алгоритма мы обрабатываем очередную одиночную переменную за линейное время, равное оставшемуся количеству переменных. А так же чтобы записать переменные, которые мы ещё не использовали тратится ещё столько же времени. Отсюда следует, что время работы линейноеквадратичное, относительно количества входящих переменных.