4446
правок
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
(не показаны 3 промежуточные версии этого же участника) | |||
Строка 16: | Строка 16: | ||
== Нотация == | == Нотация == | ||
Формула в конъюнктивно-нормальной форме представляет собой набор дизъюнктов (понимаемый как конъюнкция этих дизъюнктов), дизъюнкт – набор литералов (понимаемый как дизъюнкция этих литералов), а литерал – либо булеву переменную, либо отрицание булевой переменной. Истинностное присваивание присваивает булевы значения ('''false''' или '''true''') одной или нескольким переменным. Сокращенное присваивание представляет собой список литералов, которые при данном присваивании получают значение '''true''' (например, присваивание значения '''false''' переменной x и значения '''true''' – переменной y обозначается <math>\lnot x, y</math>). Результатом применения присваивания A к формуле F (обозначаемым F[A]) является формула, полученная удалением дизъюнктов, содержащих истинные литералы | Формула в конъюнктивно-нормальной форме представляет собой набор дизъюнктов (понимаемый как конъюнкция этих дизъюнктов), дизъюнкт – набор литералов (понимаемый как дизъюнкция этих литералов), а литерал – либо булеву переменную, либо отрицание булевой переменной. Истинностное присваивание присваивает булевы значения ('''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 называется ''выполнимой''. | ||
== Основные результаты == | == Основные результаты == | ||
Строка 25: | Строка 25: | ||
Тривиальный алгоритм перебора, перечисляющий все возможные присваивания n переменным, выполняется за <math>2^n</math> шагов с полиномиальным временем. Таким образом, <math>\alpha \le 2</math>; по тривиальной причине <math>\beta, \gamma \le 2</math>. В начале 80-х Мониен и Спекенмейер заметили, что <math>\beta</math> можно сделать меньше. ''//И они, и другие исследователи также отметили, что | Тривиальный алгоритм перебора, перечисляющий все возможные присваивания n переменным, выполняется за <math>2^n</math> шагов с полиномиальным временем. Таким образом, <math>\alpha \le 2</math>; по тривиальной причине <math>\beta, \gamma \le 2</math>. В начале 80-х Мониен и Спекенмейер заметили, что <math>\beta</math> можно сделать меньше. ''//И они, и другие исследователи также отметили, что <math>\alpha</math> можно сделать меньше для специального случая задачи, в котором длина каждого дизъюнкта ограничена константой; соответствующие ссылки и алгоритмы см. в статье «[[Алгоритмы локального поиска для k-КНФ]]».//'' | ||
Затем Куллманн и Лукхардт [12] разработали схему для алгоритмов SAT типа «разделяй и властвуй» ''//также называемых DPLL в связи со статьями Дэвиса и Патнем [7] и Дэвиса, Логемана и Лавленда [6]//'', которая разбивала исходную задачу на несколько (как правило, постоянное число) подзадач, подставляя значения некоторых переменных и упрощая полученные формулы. В результате этого исследования были получены следующие верхние пределы для <math>\beta</math> и <math>\gamma</math>: | Затем Куллманн и Лукхардт [12] разработали схему для алгоритмов SAT типа «разделяй и властвуй» ''//также называемых DPLL в силу его связи со статьями Дэвиса и Патнем [7] и Дэвиса, Логемана и Лавленда [6]//'', которая разбивала исходную задачу на несколько (как правило, постоянное число) подзадач, подставляя значения некоторых переменных и упрощая полученные формулы. В результате этого исследования были получены следующие верхние пределы для <math>\beta</math> и <math>\gamma</math>: | ||
Строка 40: | Строка 40: | ||
<math>T(F) \le \sum_{i=1}^k T(F'_i) + const,</math> | <math>T(F) \le \sum_{i=1}^k T(F'_i) + const,</math> | ||
давало желаемую верхнюю границу по количеству листьев в дереве рекуррентности и, следовательно, по времени работы алгоритма. В частности, для получения границы <math>|F|^{O(1)} \cdot 2^{0,30897m} | давало желаемую верхнюю границу по количеству листьев в дереве рекуррентности и, следовательно, по времени работы алгоритма. В частности, для получения границы <math>|F|^{O(1)} \cdot 2^{0,30897m}</math> необходимо решить либо две подзадачи F[x], F[<math>\lnot</math>x] с рекуррентным неравенством | ||
<math>t_m \le t_{m - 3} + t_{m - 4}</math> | <math>t_m \le t_{m - 3} + t_{m - 4}</math> | ||
Строка 48: | Строка 48: | ||
<math>t_m \le 2t_{m - 6} + 2t_{m - 7},</math> | <math>t_m \le 2t_{m - 6} + 2t_{m - 7},</math> | ||
где <math>t_i = max_{m(G)\le i} T(G)</math>. Правила упрощения, используемые в алгоритмах со временем выполнения <math>|F|^{O(1)} \cdot 2^{0,30897m} | где <math>t_i = max_{m(G)\le i} T(G)</math>. Правила упрощения, используемые в алгоритмах со временем выполнения <math>|F|^{O(1)} \cdot 2^{0,30897m}</math> и <math>|F|^{O(1)} \cdot 2^{0,10299l}</math>, выглядят следующим образом. | ||
Строка 107: | Строка 107: | ||
'''''Граница для <math>\gamma</math>''''' | '''''Граница для <math>\gamma</math>''''' | ||
Для получения границы <math>|F|^{O(1)} \cdot 2^{0,10299l}</math> достаточно использовать пару <math>F[\neg a], F[I(a, F)]</math> подзадач (см. лемму 2(2)), обеспечивающую необходимое рекуррентное неравенство <math>t_l \le t_{l - 5} + t_{l | Для получения границы <math>|F|^{O(1)} \cdot 2^{0,10299l}</math> достаточно использовать пару <math>F[\neg a], F[I(a, F)]</math> подзадач (см. лемму 2(2)), обеспечивающую необходимое рекуррентное неравенство <math>t_l \le t_{l - 5} + t_{l - 17}</math>, и перейти к алгоритму с временем выполнения <math>|F|^{O(1)} \cdot 2^{0,30897m}</math>, если таковой пары нет. Недавнее и намного более технически сложное улучшение этого алгоритма [16] обеспечивает границу <math>|F|^{O(1)} \cdot 2^{0,0926l}.</math> | ||
'''''Граница для <math>\alpha</math>''''' | '''''Граница для <math>\alpha</math>''''' | ||
В настоящее время нетривиальная константная верхняя граница для | В настоящее время нетривиальная константная верхняя граница для <math>\alpha</math> неизвестна. Однако, начиная с работы [14], были предложены любопытные неконстантные границы. Был разработан ряд рандомизированных и детерминированных алгоритмов, демонстрирующих последовательные улучшения. Лучшая на данный момент возможная граница достигается при помощи детерминированного алгоритма «разделяй и властвуй», применяющего следующую рекурсивную процедуру. Его идея заключается в дихотомии: либо каждый дизъюнкт входной формулы можно сократить до первых k литералов (тогда можно применить алгоритм k-КНФ), либо все эти литералы в одном из дизъюнктов можно считать ложными. Такой подход к сокращению дизъюнктов можно приписать Шулеру [15], который использовал его в рандомизированной форме. Следующая версия детерминированного алгоритма, достигающего лучшей известной границы как для детерминированных, так и для рандомизированных алгоритмов, приведена в [5]). | ||
Строка 147: | Строка 147: | ||
Основными нерешенными вопросами в данной области остаются доказательство наличия постоянной верхней границы на <math>\alpha < 2</math>, а также гипотетическое существование алгоритмов с временем выполнения <math>(1 + \varepsilon)^l</math> для произвольного малого <math>\varepsilon > 0</math>. | Основными нерешенными вопросами в данной области остаются доказательство наличия постоянной верхней границы на <math>\alpha < 2</math>, а также гипотетическое существование алгоритмов с временем выполнения <math>(1 + \varepsilon)^l</math> для произвольного малого <math>\varepsilon > 0</math>. | ||
Можно провести анализ алгоритма «разделяй и властвуй» и даже автоматически генерировать правила упрощения [10]. Однако пока такой подход позволил получить новые границы только для (NP-полной) версии оптимизации | Можно провести анализ алгоритма «разделяй и властвуй» и даже автоматически генерировать правила упрощения [10]. Однако пока такой подход позволил получить новые границы только для (NP-полной) версии оптимизации 2-КНФ [9]. | ||
== Экспериментальные результаты == | == Экспериментальные результаты == |
правок