В данном разделе рассматриваются два семейства эффективных алгоритмов пропозиционального логического вывода, основанного на проверке по модели: один подход основан на поиске с возвратами, а другой — на поиске с восхождением к вершине. Указанные алгоритмы входят в состав основного "инструментария" пропозициональной логики. Этот раздел может быть пропущен при первом чтении настоящей главы.

Рассматриваемые здесь алгоритмы предназначены для проверки выполнимости. Выше уже отмечалась связь между поиском модели, обеспечивающей выполнимость логического высказывания, и поиском решения задачи удовлетворения ограничения, поэтому, скорее всего, нет ничего удивительного в том, что эти два семейства алгоритмов весьма напоминают алгоритмы поиска с возвратами, описанные в разделе 5.2, и алгоритмы локального поиска, которые представлены в разделе 5.3. Тем не менее приведенные здесь алгоритмы являются чрезвычайно важными сами по себе, поскольку в компьютерных науках существует очень много комбинаторных задач, которые можно свести к проверке выполнимости пропозиционального высказывания. Любое усовершенствование алгоритмов проверки выполнимости влечет за собой колоссальные последствия, связанные с повышением нашей способности справляться со всеми сложными задачами в целом.