ЭФФЕКТИВНЫЙ ПРОПОЗИЦИОНАЛЬНЫЙ ЛОГИЧЕСКИЙ ВЫВОД
Аналогичным образом, высказывание является ложным, если ложно любое его выражение, а это происходит, если каждый литерал этого выражения является ложным. Опять-таки, такая ситуация может возникнуть задолго до того, как модель будет полностью составлена. Раннее завершение позволяет обойтись без исследования целых поддеревьев в пространстве поиска.
• Эвристика чистого символа. Чистым символом называется символ, который всегда появляется с одним и тем же "знаком" во всех выражениях. Например, в трех выражениях (A v -iB), (-iB v -пС) и (С v А) символ А является чистым, поскольку он появляется только в виде положительных литералов, чистым можно также считать символ в, который появляется только в виде отрицательных литералов, а символ С считается нечистым. Можно легко показать, что если некоторое высказывание имеет модель, то это — модель с чистыми символами, значения которым присвоены так, чтобы их литералы приняли значение true, поскольку при таком условии ни одно выражение не может стать ложным. Следует отметить, что при определении чистоты символа алгоритм может игнорировать выражения, в отношении которых уже известно, что они истинны в модели, составленной до сих пор. Например, если модель содержит присваивание в= false, то выражение (-iB v -.С) уже является истинным, а символ С становится чистым, поскольку присутствует только в выражении (С v А).
• Эвристика единичного выражения. Единичное выражение было определено ранее как выражение только с одним литералом. В контексте алгоритма DPLL оно также относится к выражениям, в которых в данной модели всем литералам, кроме одного, уже было присвоено значение false. Например, если модель содержит присваивание в= false, то выражение (В v -,с) становится единичным выражением, поскольку оно эквивалентно выражению [False v —1С), или просто -.С. Очевидно, для того, чтобы это выражение приняло истинное значение, литералу С должно быть присвоено значение false. Эвристика единичного выражения предусматривает присваивание значений всем таким символам до того, как происходит переход к обработке оставшейся части высказывания. Одним из важных следствий из этой эвристики является то, что любая попытка доказать (путем опровержения) истинность литерала, который уже находится в базе знаний, немедленно приводит к успеху (упр. 7.16). Следует также отметить, что присваивание значения одному единичному выражению может привести к созданию еще одного единичного выражения; например, после присваивания символу С значения false единичным становится выражение (С v А), что влечет за собой присваивание истинного значения символу А. Такое "каскадное" распространение форсированных присваиваний называется распространением единичных выражений. Оно напоминает процесс прямого логического вывода с применением хорновских выражений, а в действительности, если рассматриваемое высказывание в конъюнктивной нормальной форме содержит только хорновские выражения, то алгоритм DPLL по сути сводится к алгоритму прямого логического вывода (см. упр. 7.17).
Алгоритм DPLL приведен в листинге 7.7. В этом листинге показана самая важная структурная часть алгоритма, которая описывает сам процесс поиска, но не представлены структуры данных, которые необходимо сопровождать для обеспечения эффективности каждого этапа поиска, а также исключены все программистские "хитрости", которые можно было бы ввести для повышения производительности: изучение выражений, эвристики выбора переменных и операции рандомизированного перезапуска. После включения всех этих усовершенствований алгоритм DPLL, несмотря на свой почтенный возраст, становится одним из самых быстрых алгоритмов проверки выполнимости, которые когда-либо были разработаны. В частности, реализация Chaff этого алгоритма используется для решения задач проверки качества аппаратного обеспечения с миллионом переменных.
Листинг 7.7. Алгоритм DPLL для проверки выполнимости высказывания в пропозициональной логике. Принципы работы функций Find-Pure-Symbol и Find-Unit-Clause описаны в тексте; каждая из них возвращает символ (или неопределенное значение), а также истинностное значение, которое должно быть присвоено этому символу. Как и алгоритм TT-Entails?, этот алгоритм работает с частично составленными моделями
function DPLL-Satisfiable?(s) returns значение true или false inputs: s, высказывание в пропозициональной логике
clauses <— множество выражений высказывания s, преобразованного
в форму представления CNF symbols <г- список пропозициональных символов в высказывании s return DPLL(clauses, 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 <— First(symbols); rest <— Rest(symbols) return DPLL(clauses, rest, Extend(P, true, model)) or DPLL(clauses, rest, Extend(P, false, model))