#optimization #boolean #z3 #n-queens #sat
#оптимизация #логический #z3 #n-королевы #сидел
Вопрос:
Мне нужно преобразовать неограниченную пропозициональную формулу в CNF, а затем в 3-SAT. Я знаю Правила переписывания для перевода формул в Конъюнктивную Нормальную форму
α ↔ β (¬α ∨ β) ∧ (¬β ∨ α) α → β ¬α ∨ β (4.2) ¬(α ∨ β) ¬α ∧ ¬β (4.3) ¬(α ∧ β) ¬α ∨ ¬β (4.4) ¬¬α α (4.5) α ∨ (β ∧ γ) (α ∨ β) ∧ (α ∨ γ) (4.6) (α ∧ β) ∨ γ (α ∨ γ) ∧ (β ∨ γ Но я не понимаю, как я нахожу реальный жизненный пример концепции. Не могли бы вы помочь в реализации. Я не могу найти примера из реальной жизни. Спасибо.
На самом деле я пытаюсь показать, что неограниченные формулы могут быть преобразованы в ограниченные формы, и решение для обоих одинаково. Поэтому я пишу любую неограниченную пропозициональную формулу, преобразую ее в CNF, а затем в 3-SAT(вручную), таким образом, я могу показать аналогичный результат. Таким образом, мне нужны USAT-org и USAT-converted, где org-это неограниченная формула, а преобразованная формула в 3-CNF в качестве синтаксиса SMT (файлы SMT-LIB2)
Ответ №1:
Вы можете делать это по одному за раз. Давайте возьмем, к примеру, второй:
α → β становится:
¬α ∨ β В SMTLib вы докажете эквивалентность этих двух выражений, подтвердив отрицание их эквивалентности и проверив unsat . Идея состоит в том, что если отрицание неудовлетворительно, то эквивалентность должна соблюдаться для всех значений.
(set-option :produce-models true) (set-logic QF_BV) (declare-fun alpha () Bool) (declare-fun beta () Bool) (define-fun lhs () Bool (=gt; alpha beta)) (define-fun rhs () Bool (or (not alpha) beta)) (assert (not (= lhs rhs))) (check-sat) Это печатает:
unsat Таким образом, вышеизложенное означает, что преобразование корректно для произвольных значений alpha и beta .
Используя один и тот же трюк, вы должны доказать каждое из своих превращений. Затем это немного мета-рассуждения (или вы можете сделать ручную индукцию самостоятельно), чтобы показать, что если вы примените эти преобразования ко всем подформулам, пока все они не будут записаны, вы сможете преобразовать произвольные формулы в эту форму. Обратите внимание, что этот последний шаг не может быть выполнен непосредственно с помощью решателя SMT, так как он нуждается в индукции; но вы можете либо выполнить ручное доказательство использования правильного доказательства теоремы, такого как Isabelle/ACL2/Hol/Lean и т. Д.