Алгоритм поиска с возвратами

Привет, мой друг, тебе интересно узнать все про алгоритм поиска с возвратами, тогда с вдохновением прочти до конца. Для того чтобы лучше понимать что такое алгоритм поиска с возвратами , настоятельно рекомендую прочитать все из категории Логика.

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

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

Эвристика чистого символа. Чистым символом называется символ, который всегда появляется с одним и тем же "знаком" во всех выражениях. Например, в трех выражениях (A v ¬B), (¬B v ¬C) и (С v А) символ А является чистым, поскольку он появляется только в виде положительных литералов, чистым можно также считать символ в, который появляется только в виде отрицательных литералов, а символ С считается нечистым. Можно легко показать, что если некоторое высказывание имеет модель, то это — модель с чистыми символами, значения которым присвоены так, чтобы их литералы приняли значение true, поскольку при таком условии ни одно выражение не может стать ложным. Об этом говорит сайт https://intellect.icu . Следует отметить, что при определении чистоты символа алгоритм может игнорировать выражения, в отношении которых уже известно, что они истинны в модели, составленной до сих пор. Например, если модель содержит присваивание В- 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))

Если я не полностью рассказал про алгоритм поиска с возвратами? Напиши в комментариях Надеюсь, что теперь ты понял что такое алгоритм поиска с возвратами и для чего все это нужно, а если не понял, или есть замечания, то не стесняйся, пиши или спрашивай в комментариях, с удовольствием отвечу. Для того чтобы глубже понять настоятельно рекомендую изучить всю информацию из категории Логика