Примеры DPLL и удовлетворенности?

Мы знаем DPLL алгоритм - это откат + распространение единицы + чистое правило буквального.Примеры DPLL и удовлетворенности?

У меня есть пример. Существует один пример для решения следующей проблемы с удовлетворенностью с DPLL. если присваивание переменных «0» перед назначением «1» переменным, из которых Unit Clause (UC) или Pure Literal (PL) используется для решения этого конкретного примера?

{~A \/ B \/ C}, {A \/ ~B \/ C}, {A \/ B \/ ~C}, {A \/ B \/ C}

В этом примере написано, используя два из них (PL and UC). почему выбрали два из них? Есть идеи?

источник

2016-02-20 Math Lover

Вы знаете, что задействовано обратное отслеживание.Если остальные были только UP и PL, и от них нечего было бы отступить, потому что они не сделали бы никаких выборов, которые могут быть неправильными. – harold

@harold Вы можете использовать PL или UC. вы можете использовать один из них. – user4249446

@ user4249446, конечно, вы можете, но вы не можете * использовать * их вообще. – harold

Вот как DPLL может быть использован, чтобы решить вашу примерную формулу:

распространения блока не представляется возможным, поскольку нет ни одного блока положения.
Чистое правильное правило неприменимо, поскольку нет литералов, которые имеют место только положительно или только отрицательно.
Для применения правило расщепления выберите некоторый литерал, например. A.
- A=0 и распространяются. Это приведет к
  {1 \/ B \/ C}, {0 \/ ~B \/ C}, {0 \/ B \/ ~C}, {0 \/ B \/ C}
  == {~B \/ C}, {B \/ ~C}, {B \/ C}
- распространения Блок и чистый литерал еще не применяется.
- Применить правило разделения для следующего литерала B.
  - Набор B=0 и распространяются:
    {1 \/ C}, {0 \/ ~C}, {0 \/ C}
    == {~C}, {C}
  - Эта формула состоит из двух единичных статей, так что можно применить блок распространения, что приводит к {} поэтому мы отступиться.
  - Установить B=1 и размножаться. {0 \/ C}, {1 \/ ~C}, {1 \/ C}
    == {C}
  - Опять же, модуль распространения применим, но теперь приводит к пустой формуле, которая является тривиальным выполнима.

Какой из блока Пункта (UC) или чистого литерала (PL) используется для решения этого конкретного примера?

Распространение разложения единиц используется для решения этого примера. И из-за симметрии формулы выбор разделяющих литералов в разном порядке приведет к такому же результату.

источник

2016-02-20 12:39:16

Я уверен, что PL и UC могут решить этот пример :), но вы настолько эксперт –

PL & UC недостаточно, так как их невозможно применить без предварительного преобразования формулы. Оба работают только в том случае, если существуют специальные статьи/литералы. –

Okey, после преобразования вы говорите, что UC решить. это означает, что PL не может применяться? –

ответ

Смежные вопросы