Просмотр кода страницы Пороги для задачи выполнимости случайной k-КНФ

== Ключевые слова и синонимы ==
Фазовые переходы (''Phase transitions''); вероятностный анализ эвристики Дэвиса-Путнам (''Probabilistic analysis of a Davis-Putnam heuristic'')

== Постановка задачи ==
Рассмотрим n булевых переменных <math>V = \{ x_1, ..., x_n \}</math> и соответствующий набор из <math>2n</math> литералов <math>L = \{х_1, \bar{х}_1, ..., x_n, \bar{x}_n \} </math>. k-дизъюнктом называется дизъюнкция <math>k</math> литералов, в которую каждая переменная входит не более одного раза. Случайная формула <math>\phi_{n, m}</math> в k-конъюнктивной нормальной форме (k-КНФ) представляет собой конъюнкцию <math>m</math> дизъюнктов, каждый из которых выбирается равномерно случайным и независимым образом среди <math>2^k \tbinom{n}{k}</math> возможных k-дизъюнктов на n переменных в V. Плотностью <math>r_k</math> k-КНФ-формулы <math>\phi_{n, m}</math> называется отношение числа дизъюнктов к числу переменных m/n.


Было высказано предположение, что для каждого <math>k \ge 2</math> существует критическая плотность <math>r^*_k</math>, такая, что асимптотически почти все k-КНФ-формулы с плотностью <math>r < r^*_k \; (r > r^*_k)</math> являются выполнимыми (соответственно, невыполнимыми). До момента написания данной статьи гипотеза была доказана только для <math>k = 2</math> [3, 11]. Для <math>k \ge 3</math> гипотеза остается открытой, но подтверждается экспериментальными данными [14], а также теоретическими, но нестрогими работами, основанными на статистической механике [15]. Значение предполагаемого порога <math>r^*_3</math> оценивается примерно в 4,27. Также были вычислены приблизительные значения предполагаемого порога для больших значений k.


Что касается строгих результатов, то Фридгут [10] доказал, что для каждого <math>k \ge 3</math> существует последовательность <math>r^*_k(n)</math>, такая, что для любого <math>\epsilon > 0</math> асимптотически почти все k-КНФ формулы <math>\phi_n, _{\lfloor (r^*_k(n) - \epsilon )n\rfloor} (\phi_n, _{\lceil (r^*_k(n) + \epsilon )n \rceil} ) </math> являются выполнимыми (соответственно, невыполнимыми). Вопрос о сходимости последовательности <math>r^*_k(n), n = 0, 1, ... </math>  для <math>k \ge 3</math> остается открытым. 


Теперь положим

<math>r^{* -}_k = \underline{lim}_{n \to \infty} r^*_k(n) = sup \{ r_k: Pr [ \phi_{n, \lfloor r_k n \rfloor} </math> выполнимо <math>\to 1 ] \}</math>

и

<math>r^{* +}_k = \overline{lim}_{n \to \infty} r^*_k(n) = inf \{ r_k: Pr [ \phi_{n, \lceil r_k n \rceil} </math> выполнимо <math>\to 0 ] \}</math>.


Очевидно, что <math>r^{* -}_k \le r^{* -}_k</math>. Ограничение снизу (сверху) <math>r^{* -}_k</math> (<math>r^{* +}_k</math>, соответственно) как можно большей (как можно меньшей, соответственно) границей в последнее десятилетие стало предметом интенсивных исследований.


Верхние границы <math>r^{* +}_k</math> вычисляются путем подсчета аргументов. Если точнее, стандартная техника заключается в вычислении ожидаемого количества выполнимых истинностных присваиваний случайной формулы с плотностью <math>r_k</math> и нахождении как можно меньшего значения <math>r_k</math>, для которого это ожидаемое значение приближается к нулю. Тогда из неравенства Маркова следует, что при таком значении <math>r_k</math> случайная формула <math>\phi_n, _{\lceil (r_k n \rceil}</math> почти всегда асимптотически невыполнима. Это утверждение было уточнено в двух направлениях. 

Во-первых, рассматриваются не все выполнимые истинностные присваивания, а их подкласс, обладающий следующим свойством: выполнимая формула всегда имеет выполнимое истинностное присваивание в рассматриваемом подклассе. В силу ограничения на рациональный выбор такого подкласса ожидаемое значение количества выполнимых истинностных присваиваний приближается к вероятности выполнимости и, таким образом, приводит к получению лучшей (меньшей) верхней границы <math>r_k</math>. Однако важно, чтобы подкласс был таким, чтобы ожидаемое значение количества выполнимых истинностных присваиваний можно было вычислить с помощью доступных вероятностных техник.

Во-вторых, при вычислении ожидаемого количества выполнимых истинностных присваиваний следует использовать ''типичные'' характеристики случайной формулы, то есть характеристики, общие для асимптотически почти всех формул. Опять же, это часто приводит к тому, что ожидаемое количество выполнимых истинностных присваиваний оказывается ближе к вероятности выполнимости (нетипичные формулы могут способствовать увеличению ожидаемого количества). Значительно более хорошие верхние границы для <math>r_3^{* +}</math> были вычислены путем подсчета аргументов, как указано выше (см. обзоры [6, 13]). Дюбуа, Буфхад и Мандлер [7] доказали, что <math>r_3^{*+} < 4,506</math>. Это лучшая верхняя граница на момент написания статьи.


С другой стороны, для фиксированных и малых значений k (особенно для k = 3) нижние границы <math>r^{* -}_k</math> обычно вычисляются алгоритмическими методами. Точнее, конструируется алгоритм, который для как можно большего <math>r_k</math> выдает выполнимое истинностное присваивание для асимптотически почти всех формул <math>\phi_n, _{\lfloor (r_k n \rfloor}</math>. Такое <math>r_k</math>, очевидно, является нижней границей <math>r_k^{*-}</math>. Чем проще алгоритм, тем легче провести вероятностный анализ выдачи выполнимого истинностного присваивания для заданного <math>r_k</math>, но тем меньше <math>r_k</math>, для которого почти всегда асимптотически выдается выполнимое истинностное присваивание. В этом контексте были тщательно проанализированы алгоритмы DPLL без возвратов [4, 5] все большей сложности (см. обзоры [2, 9]). На каждом шаге такого алгоритма литералу задается значение TRUE, а затем выводится ''приведенная'' формула путем (1) удаления дизъюнктов, в которых встречается этот литерал, и (2) удаления отрицания этого литерала из дизъюнктов, в которых оно встречается. На тех шагах, где существуют 1-дизъюнкты (так называемые вынужденные шаги), выбор литерала, который должен получить значение TRUE, осуществляется таким образом, чтобы 1-дизъюнкт стал выполнимым. На остальных шагах (называемых свободными) выбор литерала, который должен получить значение TRUE, осуществляется в соответствии с эвристикой, определяемой конкретным алгоритмом DPLL. За свободным шагом следует раунд последовательных вынужденных шагов. Для упрощения вероятностного анализа алгоритмов DPLL предполагается отсутствие у них возвратов: если алгоритм натыкается на противоречие, т. е. генерируется 0-дизъюнкт, он останавливает выполнение и сообщает о сбое, в противном случае он выдает выполнимое истинностное присваивание. Лучшая нижняя граница для порога выполнимости, полученная в результате такого анализа, составила <math>3,26 < r_3^{*-}</math> (Ахлиоптас и Соркин [1]).


Проанализированные ранее подобные алгоритмы (за исключением алгоритма Pure Literal [8]) на свободном шаге учитывают только размер дизъюнкта, в котором встречается выбранный литерал. Благодаря этой ограниченности информации, используемой при выборе получающего значение литерала, приведенная формула на каждом шаге остается случайной, обусловленной только текущим количеством 3- и 2-дизъюнкт и количеством переменных, еще не получивших присваивание. Такое сохранение «сильной» случайности позволяет провести успешный вероятностный анализ алгоритма достаточно несложным способом. Однако для k = 3 удается показать выполнимость только для плотностей, слегка превышающих 3,26. В частности, в [1] было показано, что это оптимальное значение, которое может быть достигнуто подобными алгоритмами.

== Основные результаты ==
В работе [12] был описан (и затем проанализирован с вероятностной точки зрения) алгоритм DPLL, в котором на каждом свободном шаге литерал, которому должно быть задано значение TRUE, выбирается с учетом его ''степени'' (т. е. количества вхождений) в текущей формуле.


'''Алгоритм Greedy (глава 4.A в [12])'''

Первый вариант алгоритма очень прост: на каждом свободном шаге выбирается литерал с максимальным количеством вхождений, и ему задается значение TRUE. Заметим, что в этом жадном варианте литерал выбирается независимо от количества вхождений его отрицания. Этот алгоритм успешно выдает выполнимое истинностное присваивание для асимптотически почти всех формул с плотностью до числа, немного большего 3,42, устанавливая, что <math>r_3^{*-} > 3,42</math>. Его простота, контрастирующая с улучшением по сравнению с ранее полученными нижними границами, говорит о важности анализа эвристик, учитывающих информацию о степени текущей формулы.
 

'''Алгоритм CL (глава 5.A в [12])'''

Во втором варианте на каждом свободном шаге ''t'' также учитывается степень отрицания <math>\bar{\tau}</math> литерала <math>\tau</math>, которому задано значение TRUE. Точнее говоря, литерал, которому задается значение TRUE, выбирается таким образом, чтобы по завершении раунда вынужденных шагов, следующих за свободным шагом ''t'', предельное ожидаемое увеличение потока от 2-дизъюнктов к 1-дизъюнктам на единицу ожидаемого уменьшения потока от 3-дизъюнктов к 2-дизъюнктам было минимальным. Предельное значение математического ожидания, соответствующее каждому литералу, может быть вычислено из количества его положительных и отрицательных вхождений. Более конкретно, если <math>m_i, i = 2, 3</math> равно ожидаемому потоку от i-дизъюнктов к (i - 1)-дизъюнктам на каждом шаге раунда, а <math>\tau</math> – литерал, которому в начале раунда присвоено значение TRUE, то <math>\tau</math> выбирается таким образом, чтобы минимизировать отношение <math>| \frac{\Delta m_2}{\Delta m_3} |</math> разностей <math>\Delta m_2</math> и <math>\Delta m_3</math> между началом и концом раунда. Следствием этого является ограничение скорости генерации 1-дизъюнктов наименьшим возможным числом на протяжении всего алгоритма. Для успешности вероятностного анализа нам нужно знать для каждых значений ''i, j'' количество литералов степени ''i'', отрицание которых имеет степень ''j''. Эта эвристика успешно выдает выполнимое истинностное присваивание для асимптотически почти всех формул с плотностью до числа, немного большего 3,52, устанавливая, что <math>r_3^{*-} > 3,52</math>.

== Применение ==
SAT-решатели (программы для решения задачи выполнимости булевых формул) применяются, в частности, в таких областях, как верификация последовательных цепей, искусственный интеллект, автоматическое вычисление и планирование, СБИС, САПР, проверка моделей и другие виды формальной верификации. Недавно автоматические методы проверки моделей на основе SAT начали использоваться для эффективного выявления атак на протоколы безопасности.

== Открытые вопросы ==
Главной нерешенной проблемой в этой области является формальное доказательство существования порога <math>r^*_k</math> для всех (или хотя бы некоторых) <math>k \ge 3</math>. Строгое вычисление верхних и нижних границ, лучших, чем упомянутые выше, также вызывает определенный интерес. Связанные с этим результаты и проблемы возникают в рамках вариантов задачи выполнимости, а также проблемы раскрашиваемости.

== См. также ==
* [[k-КНФ-алгоритмы на базе поиска с возвратом]]
* [[Алгоритмы локального поиска для k-КНФ]]
* [[Максимальная выполнимость формул в 2-КНФ]]
* [[Границы хвостов для задач о размещении]]
 
== Литература ==
1.	Achioptas, D., Sorkin,G.B.: Optimal myopic algorithms for random 3-sat. In: 41st Annual Symposium on Foundations of Computer Science, pp. 590-600. IEEE Computer Society, Washington (2000)

2.	Achlioptas, D.: Lower bounds for random 3-sat via differential equations. Theor. Comput. Sci. 265(1-2), 159-185 (2001)

3.	Chvatal,V., Reed, B.: Mick gets some (the odds are on his side). In: 33rd Annual Symposium on Foundations of Computer Science, pp. 620-627. IEEE Computer Society, Pittsburgh (1992)

4.	Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5, 394-397 (1962)

5.	Davis, M., Putnam, H.: A computing procedure for quantification theory. J. Assoc. Comput. Mach. 7(4), 201 -215 (1960)

6.	Dubois, O.: Upper bounds on the satisfiability threshold. Theor. Comput. Sci. 265,187-197 (2001)

7.	Dubois, O., Boufkhad, Y., Mandler, J.: Typical random 3-sat formulae and the satisfiability threshold. In: 11 th ACM-SIAM symposium on Discrete algorithms, pp. 126-127. Society for Industrial and Applied Mathematics, San Francisco (2000)

8.	Franco, J.: Probabilistic analysis of the pure literal heuristic for the satisfiability problem. Annal. Oper. Res. 1, 273-289 (1984)

9.	Franco, J.: Results related to threshold phenomena research in satisfiability: Lower bounds. Theor. Comput. Sci. 265,147-157 (2001)

10.	Friedgut, E.: Sharp thresholds of graph properties, and the k-sat problem. J. AMS 12,1017-1054 (1997)

11.	Goerdt, A.: A threshold for unsatisfiability. J. Comput. Syst. Sci. 33,469^86(1996)

12.	Kaporis, A.C., Kirousis, L.M., Lalas, E.G.: The probabilistic analysis of a greedy satisfiability algorithm. Random Struct. Algorithms 28(4), 444-480 (2006)

13.	Kirousis, L., Stamatiou, Y., Zito, M.: The unsatisfiability threshold conjecture: the techniques behind upper bound improvements. In: A. Percus, G. Istrate, С Moore (eds.) Computational Complexity and Statistical Physics, Santa Fe Institute Studies in the Sciences of Complexity, pp. 159-178. Oxford University Press, New York (2006)

14.	Mitchell, D., Selman, B., Levesque, H.: Hard and easy distribution of sat problems. In: 10th National Conference on Artificial Intelligence, pp. 459^65. AAAI Press, Menlo Park (1992)

15.	Monasson, R., Zecchina, R.: Statistical mechanics of the random k-sat problem. Phys. Rev. E 56,1357-1361 (1997)