Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида: различия между версиями
Перейти к навигации
Перейти к поиску
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) Нет описания правки |
||
| Строка 16: | Строка 16: | ||
== Нотация == | == Нотация == | ||
Формула в конъюнктивно-нормальной форме представляет собой набор дизъюнктов (понимаемый как конъюнкция этих дизъюнктов), дизъюнкт – набор литералов (понимаемый как дизъюнкция этих литералов), а литерал – либо булеву переменную, либо отрицание булевой переменной. Истинностное присваивание присваивает булевы значения ( | Формула в конъюнктивно-нормальной форме представляет собой набор дизъюнктов (понимаемый как конъюнкция этих дизъюнктов), дизъюнкт – набор литералов (понимаемый как дизъюнкция этих литералов), а литерал – либо булеву переменную, либо отрицание булевой переменной. Истинностное присваивание присваивает булевы значения ('''false''' или '''true''') одной или нескольким переменным. Сокращенное присваивание представляет собой список литералов, которые при данном присваивании получают значение '''true''' (например, присваивание значения '''false''' переменной x и значения '''true''' – переменной y обозначается <math>\lnot x, y</math>). Результатом применения присваивания A к формуле F (обозначаемым F[A]) является формула, полученная удалением дизъюнктов, содержащих истинные литералы из F, и удалением ставших ложными литералов из оставшихся дизъюнктов. К примеру, если <math>F = (x \lor \lnot y \lor z) \land (y \lor \lnot z)</math>, то <math>F[ \lnot x, y] = (z)</math>. Присваиванием, обеспечивающим выполнимость формулы F, называется присваивание A, такое, что F[A] = true. Если такое присваивание существует, формула F называется ''выполнимой''. | ||
== Основные результаты == | == Основные результаты == | ||
Границы для / | |||
Общий подход и граница для / | Границы для <math>\beta</math> и <math>\gamma</math> | ||
Общий подход и граница для <math>\gamma</math> | |||