Главная arrow Знания и рассуждения arrow Алгоритм поиска с возвратами
Как начинался компьютер
Компьютерная революция
Двоичный код
Разработки военных лет
Интегральные микросхемы
Микрокомпьютер
Персоны
Сеть
Язык компьютера
Развитие ПО
Гибкие системы
Средства разработки
Информатика
Вычислительная наука
Операционные системы
Искусственный интеллект
Предыстория
Поиск
Знания и рассуждения
Логика
Робототехника
 

 
Алгоритм поиска с возвратами Печать

Первый рассматриваемый здесь алгоритм часто называют алгоритмом Дэвиса-Патнем в честь авторов оригинальной статьи, в которой он был опубликован, Мартина Дэвиса и Хилари Патнем. Затем этот алгоритм фактически стал одной из версий, описанных Дэвисом, Логеманом и Лавлендом, поэтому мы будем называть его DPLL по первым буквам фамилий всех четырех авторов. Алгоритм DPLL принимает на входе некоторое высказывание в конъюнктивной нормальной форме — высказывание, представленное как множество выражений. Как и алгоритмы Backtracking-Search и TT-Entails?, он фактически выполняет рекурсивный перебор в глубину всех возможных моделей. Но в этом алгоритме реализованы три описанных ниже усовершенствования, и этим он отличается от простой схемы, применяемой в алгоритме TT-Entails?.

Раннее завершение. Алгоритм обнаруживает, должно ли данное высказывание быть истинным или ложным, даже с помощью частично завершенной модели. Выражение является истинным, если истинен любой его литерал, даже притом что для других литералов еще не определены истинностные значения; поэтому об истинности всего высказывания в целом можно судить еще до того, как модель будет составлена полностью. Например, высказывание {A v B) л (A v С) является истинным, если истинен литерал А, независимо от значений литералов В и С. Аналогичным образом, высказывание является ложным, если ложно любое его выражение, а это происходит, если каждый литерал этого выражения является ложным. Опять-таки, такая ситуация может возникнуть задолго до того, как модель будет полностью составлена. Раннее завершение позволяет обойтись без исследования целых поддеревьев в пространстве поиска.

Эвристика чистого символа. Чистым символом называется символ, который всегда появляется с одним и тем же "знаком" во всех выражениях. Например, в трех выражениях (A v ¬B), (¬B v ¬C) и (С v А) символ А является чистым, поскольку он появляется только в виде положительных литералов, чистым можно также считать символ в, который появляется только в виде отрицательных литералов, а символ С считается нечистым. Можно легко показать, что если некоторое высказывание имеет модель, то это — модель с чистыми символами, значения которым присвоены так, чтобы их литералы приняли значение true, поскольку при таком условии ни одно выражение не может стать ложным. Следует отметить, что при определении чистоты символа алгоритм может игнорировать выражения, в отношении которых уже известно, что они истинны в модели, составленной до сих пор. Например, если модель содержит присваивание В- false, то выражение (¬B v ¬С) уже является истинным, а символ С становится чистым, поскольку присутствует только в выражении (С v А).

Эвристика единичного выражения. Единичное выражение было определено ранее как выражение только с одним литералом. В контексте алгоритма DPLL оно также относится к выражениям, в которых в данной модели всем литералам, кроме одного, уже было присвоено значение false. Например, если модель содержит присваивание B = false, то выражение (В v ¬C) становится единичным выражением, поскольку оно эквивалентно выражению (False v ¬C), или просто ¬C. Очевидно, для того, чтобы это выражение приняло истинное значение, литералу С должно быть присвоено значение false. Эвристика единичного выражения предусматривает присваивание значений всем таким символам до того, как происходит переход к обработке оставшейся части высказывания. Одним из важных следствий из этой эвристики является то, что любая попытка доказать (путем опровержения) истинность литерала, который уже находится в базе знаний, немедленно приводит к успеху. Следует также отметить, что присваивание значения одному единичному выражению может привести к созданию еще одного единичного выражения; например, после присваивания символу С значения false единичным становится выражение (С v А), что влечет за собой присваивание истинного значения символу А. Такое "каскадное" распространение форсированных присваиваний называется "&. распространением единичных выражений. Оно напоминает процесс прямого логического вывода с применением хорновских выражений, а в действительности, если рассматриваемое высказывание в конъюнктивной нормальной форме содержит только хорновские выражения, то алгоритм DPLL по сути сводится к алгоритму прямого логического вывода.

Алгоритм DPLL приведен в листинге. В этом листинге показана самая важная структурная часть алгоритма, которая описывает сам процесс поиска, но не представлены структуры данных, которые необходимо сопровождать для обеспечения эффективности каждого этапа поиска, а также исключены все программистские "хитрости", которые можно было бы ввести для повышения производительности: изучение выражений, эвристики выбора переменных и операции рандомизированного перезапуска. После включения всех этих усовершенствований алгоритм DPLL, несмотря на свой почтенный возраст, становится одним из самых быстрых алгоритмов проверки выполнимости, которые когда-либо были разработаны. В частности, реализация Chaff этого алгоритма используется для решения задач проверки качества аппаратного обеспечения с миллионом переменных.

Алгоритм DPLL для проверки выполнимости высказывания в пропозициональной логике. Принципы работы функций Find-Pure-Symbol и Find-Unit-Clause описаны в тексте; каждая из них возвращает символ (или неопределенное значение), а также истинностное значение, которое должно быть присвоено этому символу. Как и алгоритм тт-Entails?, этот алгоритм работает с частично составленными моделями

 

function DPLL-Satisfiable?(s) returns значение true или false

  inputs: s, высказывание в пропозициональной логике

  clauses <— множество выражений высказывания s, преобразованного

  в форму представления CNF

  symbols <— список пропозициональных символов в высказывании s

  return DPLL{clausesf symbols, [])

 

function DPLL(clauses, symbols, model) returns значение true или false

  if каждое выражение в множестве clauses имеет значение true

  в модели model

  then return true

  if какое-то выражение в множестве clauses имеет значение false

  в модели model

  then return false

  P, value <— Find-Pure-Symbol(symbols, clauses, model)

  if значение P не является пустым

  then return DPLL(clauses,symbols-P,Extend(P,value,model))

  P, value <— Find-Unit-Clause(clauses, model)

  if значение P не является пустым

  then return DPLL(clauses,symbols-P,Extend(P,value,model))

  P <r- First (symbols) ; rest <— Rest (symbols)

return DPLL(clauses, rest, Extend(P, true, model)) or

            DPLL(clauses, rest, Extend(P, false, model))