"Фазовый переход" в процессе определения выполнимости сформированных случайным образом задач k-SAT впервые был обнаружен Саймоном и Дюбуа [1421]. Эмпирические результаты, полученные Кроуфордом и Отоном [307], свидетельствуют о том, что при решении крупных сформированных случайным образом задач 3-SAT это резкое изменение характеристик возникает в диапазоне значений отношения "высказывание/переменная", приближающихся к 4,24; кроме того, в этой статье описана очень эффективная реализация алгоритма DPLL. Байардо и Шрэг [87] описали еще одну эффективную реализацию алгоритма DPLL с использованием методов из области удовлетворения ограничений, а в [1090] описан алгоритм Chaff, который решает задачи проверки аппаратного обеспечения с миллионом переменных, ставший победителем конкурса SAT 2002. Ли и Энбулаган [926] описали эвристики, основанные на распространении единичных выражений, позволяющие создавать быстрые решатели задач. Чизман и др. [244] предоставили данные о многих задачах, связанных с задачами проверки выполнимости, и пришли к выводу, что все NP-трудные задачи обнаруживают фазовый переход. Кёр-кпатрик и Селман [800] показали, каким образом можно использовать методы статистической физики для получения представления о том, какова точная "форма" фазового перехода. Теоретический анализ его местонахождения все еще довольно неудовлетворителен: до сих пор удалось доказать лишь то, что для случайно сформированных задач 3-SAT фазовый переход находится в диапазоне [3.003,4.598]. Кук и Митчелл [290] составили превосходный обзор результатов по этой и некоторым другим темам, касающимся выполнимости.

Самые ранние теоретические исследования показали, что алгоритм DPLL применительно к некоторым естественным распределениям задач характеризуется в среднем полиномиальной сложностью. Этот факт, который мог бы, в принципе, стать предметом восхищения, начал казаться менее восхитительным, когда Франко и Па-улл [494] показали, что те же задачи можно было бы решить за постоянное время, просто проверяя случайно выбранные варианты присваивания. Метод случайной выработки вариантов, описанный в данной главе, приводит к получению гораздо более трудных задач. Заинтересовавшись достигнутым на практике успехом в использовании локального поиска при решении таких задач, Кутсупиас и Пападимит-риу [848] показали, что простой алгоритм восхождения к вершине способен решать почти все экземпляры задачи проверки выполнимости очень быстро, а это свидетельствует о том, что трудные задачи встречаются редко. Более того, Шёнинг [1365] продемонстрировал рандомизированный вариант алгоритма GSAT, для которого ожидаемое время прогона в худшем случае при решении задач 3-SAT составляет ; этот предел все еще является экспоненциальным, но гораздо более низким по сравнению с достигнутыми ранее пределами для худшего случая. Алгоритмы проверки выполнимости все еще остаются очень активной областью исследования; хорошей отправной точкой для изучения этой темы может служить сборник статей под редакцией Дю и др. [418].