Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида: различия между версиями

Перейти к навигации Перейти к поиску
Строка 25: Строка 25:




Тривиальный алгоритм перебора, перечисляющий все возможные присваивания n переменным, выполняется за 2n шагов с полиномиальным временем. Таким образом, a < 2, а по тривиальным причинам и f$,y < 2. В начале 1980-х Мониен и Спекенмейер заметили, что /3 можно сделать меньше1. Затем Куллманн и Лукхардт [12] разработали схему для алгоритмов SAT типа «разделяй и властвуй2», которая разбивала исходную задачу на несколько (как правило, постоянное число) подзадач, подставляя значения некоторых переменных и упрощая полученные формулы. В результате этого исследования были получены следующие верхние пределы для f$ и y.
Тривиальный алгоритм перебора, перечисляющий все возможные присваивания n переменным, выполняется за <math>2^n</math> шагов с полиномиальным временем. Таким образом, <math>\alpha \le 2</math>; по тривиальной причине <math>\beta, \gamma \le 2</math>. В начале 80-х Мониен и Спекенмейер заметили, что <math>\beta</math> можно сделать меньше. ''//И они, и другие исследователи также отметили, что a можно сделать меньше для специального случая задачи, в котором длина каждого дизъюнкта ограничена константой; соответствующие ссылки и алгоритмы см. в статье «Алгоритмы локального поиска для k-КНФ».//''
Затем Куллманн и Лукхардт [12] разработали схему для алгоритмов SAT типа «разделяй и властвуй» ''//также называемых DPLL в связи со статьями Дэвиса и Патнем [7] и Дэвиса, Логемана и Лавленда [6]//'', которая разбивала исходную задачу на несколько (как правило, постоянное число) подзадач, подставляя значения некоторых переменных и упрощая полученные формулы. В результате этого исследования были получены следующие верхние пределы для <math>\beta</math> и <math>\gamma</math>:




1 И они, и другие исследователи также заметили, что a можно сделать меньше для специального случая задачи, в котором длина каждого дизъюнкта ограничена константой; соответствующие ссылки и алгоритмы см. в статье «Алгоритмы локального поиска для k-КНФ».
Теорема 1 (Хирш [8]). Задачу SAT можно решить за время
 
2 Этот алгоритм также носит название DPLL в связи со статьями Дэвиса и Патнем [7] и Дэвиса, Логемана и Лавленда [6].
 
 
Теорема 1 (Хирш [ ]). Задачу SAT можно решить за время
1. jFjO(1). 2°:30897m;
1. jFjO(1). 2°:30897m;
2. jFjO(1) • 20:10299
2. jFjO(1) • 20:10299
Источник — http://pco.iis.nsk.su/wega/index.php/Точные_алгоритмы_решения_задачи_о_выполнимости_формулы_в_КНФ_общего_вида