Первый пример, который приходит на ум, - это объединение всех возможных дизъюнкций, содержащих каждую переменную один раз. Например, если ваши переменные p1, p2 и p3:
(¬p1 ∨ ¬p2 ∨ ¬p3) ∧ (¬p1 ∨ ¬p2 ∨ p3) ∧ (¬p1 ∨ p2 ∨ ¬p3) ∧ (¬p1 ∨ p2 ∨ p3) ∧ (p1 ∨ ¬p2 ∨ ¬p3) ∧ (p1 ∨ ¬p2 ∨ p3) ∧ (p1 ∨ p2 ∨ ¬p3) ∧ (p1 ∨ p2 ∨ p3)
Другой способ описать это: соединение отрицаний всех возможных назначений. Например, ¬ (p1 ∧ p2 ∧ p3) = (¬p1 ∨ ¬p2 ∨ ¬p3) - часть формулы. Таким образом, каждое возможное присвоение не может удовлетворить ровно одно предложение. Однако мы знаем это только потому, что убедились в том, что пункты являются исчерпывающими.
Если мы попытаемся преобразовать в каноническую дизъюнктивную нормальную форму, мы не сможем сделать это быстрее, независимо от того, в каком порядке мы пробуем переменные, и в конечном итоге получим:
(p1 ∧ ¬p1 ∧ p2 ∧ p3) ∨ (p1 ∧ p2 ∧ ¬p2 ∧ p3) ∨ (p1 ∧ p2 ∧ p3 ∧ ¬p3)
Где каждое предложение, которое мы генерируем, оказывается неудовлетворительным, но мы видим это только тогда, когда расширяем их все. Если мы попытаемся найти удовлетворительное назначение, независимо от того, в каком порядке мы пробуем переменные, мы сможем полностью проверить каждое возможное назначение только за экспоненциальное время.
Там может быть SAT-решатель, который проверяет этот особый случай, хотя проверка того, что все возможные предложения находятся во входных данных, сама по себе займет экспоненциальное время, и преобразование произвольных входных данных в каноническую форму, где вы могли бы эффективно сказать, что существует только восемь возможные предложения трех переменных, и мы уже проверили, что нет дубликатов, тоже займет некоторое время.
person
Davislor
schedule
27.09.2020
