Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида
Ключевые слова и синонимы
Задача выполнимости булевых формул (SAT)
Постановка задачи
Задача выполнимости (SAT) булевых формул в конъюнктивной нормальной форме (КНФ) является одной из первых NP-полных задач [2,13]. Поскольку NP-полнота в настоящее время не оставляет надежды на использование алгоритмов с полиномиальным временем выполнения, прогресс достигается за счет уменьшения показателя степени. Существует несколько версий этой параметризованной задачи, которые различаются параметром, используемым для оценки времени выполнения.
Задача 1 (SAT). Дано: формула F в КНФ, содержащая n переменных, m дизъюнктов clauses и l литералов.
Требуется: выдать «Да», если F содержит присваивание, обеспечивающее выполнимость формулы, т. е. подстановку булевых значений переменных, с которой значение F становится истинным, и «Нет» в противном случае.
Границы времени выполнения алгоритмов SAT, таким образом, можно выразить в форме |F|O(1) • a", |F|O(1) ■ pm, или | F\ °W ■ уl, где |F| – длина удовлетворительного битового представления F (т. е. формальных входных данных алгоритма). Фактически для существущих алгоритмов базы /3 и у являются константами, а a – функцией a(n, m) от параметров формулы (поскольку не известно лучшей константы, чем a = 2).
Нотация
Формула в конъюнктивно-нормальной форме представляет собой набор дизъюнктов (понимаемый как конъюнкция этих дизъюнктов), дизъюнкт – набор литералов (понимаемый как дизъюнкция этих литералов), а литерал – либо булеву переменную, либо отрицание булевой переменной. Истинностное присваивание присваивает булевы значения («истина» или «ложь») одной или нескольким переменным. Сокращенное присваивание представляет собой список литералов, которые при данном присваивании получают значение «истина» (например, присваивание значения «ложь» переменной x и значения «истина» – переменной y обозначается :x; y). Результатом применения присваивания A к формуле F (обозначаемым F[A]) является формула, полученная удалением дизъюнктов, содержащих истинные литералы из F, и удалением ставших ложными литералов из оставшихся дизъюнктов. К примеру, если F = (x _ :y _ z) Л ( y _:z), то F[:x; y] = (z). Присваиванием, обеспечивающим выполнимость формулы F, называется присваивание A, такое, что F[A] = true. Если такое присваивание существует, формула F называется выполнимой.
Основные результаты
Границы для /? и у Общий подход и граница для /?