Пропозициональная формула в DNF может быть решена в полиномиальное время?
-
16-10-2019 - |
Вопрос
Для данной пропозициональной формулы F в DNF можно решить в полиномиальное время, если формула удовлетворена: просто пройдите по всем субфорфулу (L_1 и ... и L_K) и проверьте, у нее нет дополнительной пары литералов. Формула F является удовлетворенной, если существует такая субформла.
Мой подход выше правильный?
Если да, мне интересно, почему все современные решатели SAT получают CNF в качестве входного формата, и не просто используют DNF.
Решение
Преобразование из CNF в DNF может привести к экспоненциальной стоимости. Например, $ (a_1 lor b_1) land cdots land (a_n lor b_n) $ расширяется до $ 2^n $ много терминов. По мере того, как вы комментируете, для удовлетворения DNF проста - это фальсифицируемость, которая сложно. Если проблема тривиальна, вы не вводите ее в решатель SAT, и именно поэтому SAT решатели принимают CNF вместо DNF.
Если вы считаете, что P отличается от NP, то это подразумевает, что не существует полиномиального способа преобразования удовлетворенности CNF в удовлетворенность DNF, поскольку первое является NP-полным, в то время как последний находится в P.