Истинностные таблицы как метод проверки допустимости или невыполнимости высказываний в языке пропозициональной логики были введены в арсенал ученых независимо Людвигом Виттгенштейном [1607] и Эмилем Постом [1231]. В 1930-х годах большие успехи были достигнуты в области создания методов логического вывода для логики первого порядка. В частности, Гёдель [565] показал, что полная процедура логического вывода в логике первого порядка может быть получена путем сведения к пропозициональной логике с использованием теоремы Эрбрана [650]. Мы снова вернемся к этой теме в главе 9, а здесь необходимо сделать важное замечание о том, что разработка эффективных пропозициональных алгоритмов в 1960-х годах мотивировалась в основном стремлением математиков создать эффективные средства доказательства теорем для логики первого порядка. Алгоритм Дэвиса— Патнем [336] был первым эффективным алгоритмом логического вывода в пропозициональной логике, но в большинстве случаев обладал меньшей эффективностью по сравнению с алгоритмом поиска с возвратами DPLL, который был введен двумя годами позже [335]. Полное правило резолюции и доказательство его полноты было опубликовано в оригинальной статье Дж.Э. Робинсона [1298], который также показал, как может осуществляться формирование рассуждений в логике первого порядка без обращения к пропозициональным методам.

Стефен Кук [289] показал, что задача определения выполнимости высказывания в пропозициональной логике является NP-полной. Поскольку определение того, является ли высказывание логическим следствием, эквивалентно задаче определения его невыполнимости, эта задача является ko-NP-полной. Известны многие подмножества пропозициональной логики, для которых задача проверки выполнимости решается за полиномиальное время; одним из таких подмножеств являются хорновские выражения. Алгоритм прямого логического вывода для хорновских выражений с линейными затратами времени предложен Доулингом и Галльером [407], которые описали свой алгоритм в виде процесса обработки потока данных, подобного распространению сигналов в логической схеме. Задача проверки выполнимости стала одним из канонических примеров сведения к NP-полным задачам; например, Кайе [782] показал, что игра Minesweeper (минный тральщик) является NP-полной.

Попытки применения алгоритмов локального поиска для решения задач проверки выполнимости предпринимались различными авторами на протяжении всех 1980-х годов; все эти алгоритмы были основаны на идее минимизации количества невыполненных выражений [614]. Особенно эффективный алгоритм был разработан Гу [601] и независимо от него Селманом и др. [1382], которые назвали этот алгоритм GSAT и показали, что он способен решать широкий перечень очень трудных задач с очень большой скоростью. Алгоритм WalkSAT, описанный в этой главе, также предложен Селманом и др. [1380].