Почему CNF используется для SAT, а не DNF?

Я не совсем понимаю, почему почти все решатели SAT используют CNF вместо DNF. Мне кажется, что решение SAT проще с использованием DNF. В конце концов, вам просто нужно просмотреть набор импликантов и проверить, содержит ли один из них и переменную, и ее отрицание. Для CNF не существует такой простой процедуры.

Сокращение учебника с SAT до 3SAT, благодаря Карпу, преобразует произвольную булеву формулу в «эквивалентную» булеву формулу CNF Φ ′ полиномиального размера , так что Φ выполнимо тогда и только тогда, когда Φ ′ выполнимо. (Строго говоря, эти две формулы не эквивалентны, так как Φ ' имеет дополнительные переменные, но значение Ф ' фактически не зависит от этих новых переменных.)$\Phi$$\Phi'$ $\Phi$$\Phi'$$\Phi'$$\Phi'$

Подобного сокращения из произвольных логических формул в формулы DNF не известно; Все известные преобразования увеличивают размер формулы в геометрической прогрессии. Более того, если P = NP, такое сокращение невозможно!

Большинство важных вещей было сказано, но я хотел бы подчеркнуть несколько моментов.

1. выполнимость формулы DNF является P
2. выполнимость формулы CNF является NP
3. тестирование, если формула CNF тавтология P
4. тестирование, если формула DNF является тавтологией, является coNP
5. отрицание DNF приводит к получению CNF и наоборот

Таким образом, решатели SAT используют CNF, потому что они нацелены на удовлетворяемость, и любая формула может быть преобразована в CNF, сохраняя выполнимость в линейном времени.

SAT решатели не «используют» CNF - им (часто) дают CNF в качестве входных данных и делают все возможное, чтобы решить CNF, который им дают. Как указывает ваш вопрос, репрезентация - это все - гораздо проще определить, удовлетворяет ли DNF, чем CNF такого же размера.

Это приводит к вопросу о том, почему решатели SAT не могут просто превратить данный CNF в DNF и решить получившийся DNF, и попытка сделать это - хорошее упражнение для понимания проблем представления.

7 - ^го сентября 2013: добавлен Далее ответ, проверка внизу страницы

---

По сути, формула DNF является дизъюнкцией пунктов , где каждый пункт c i = l i , 1 ∧ . , , ∧ л я , к является конъюнкция литералов. Давайте называть положение с я конфликтующим тогда и только тогда , когда оно содержит как буквальный л и его отрицание ¬ л . Легко видеть, что каждое неконфликтующее предложение просто кодирует 2 n - $c_1 \lor ... \lor c_m$$c_i = l_{i,1} \land ... \land l_{i,k}$$c_i$$l$$\lnot l$$2^{n-k}$Решения формулы. Таким образом, весь DNF - это просто перечень решений. Формула может иметь экспоненциально много решений, поэтому соответствующая формула DNF может иметь экспоненциально много предложений. Попробуйте преобразовать эту формулу CNF:

$l_1 \lor l_2 \lor l_3 \lor l_4$

$l_5 \lor l_6 \lor l_7 \lor l_8$

$l_9 \lor l_{10} \lor l_{11} \lor l_{12}$

$l_{13} \lor l_{14} \lor l_{15} \lor l_{16}$

$l_{17} \lor l_{18} \lor l_{19} \lor l_{20}$

к соответствующей формуле DNF: вы получите слишком много предложений. Одним словом: CNF компактен, а DNF нет; CNF неявный, а DNF явный.

Следующая проблема является NP-полной: если дан экземпляр DNF, существует ли присвоение переменных, которое искажает все предложения?

Я только что понял еще одну вещь, которая, надеюсь, заслуживает отдельного ответа. Презумпция вопроса не совсем верна. Диаграмма двоичного решения (BDD) может рассматриваться как компактное / уточненное представление DNF. Были некоторые SAT решатели, использующие BDD, но я считаю, что они больше не появляются.

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

Этот дальнейший ответ подразумевает обратную связь с комментарием divybyzero к моему предыдущему ответу.

Как говорит DivideByzero, это, безусловно, правда, что CNF и DNF являются двумя сторонами одной медали.

Когда вам нужно найти удовлетворяющее назначение, DNF является явным, поскольку оно явно показывает вам свои удовлетворяющие назначения (DNF Удовлетворенность принадлежит ), тогда как CNF является неявным, поскольку оно скрывает и удовлетворяет ваши удовлетворяющие назначения от ваших глаз (CNF Удовлетворенность равна N Р - с о м п л е т е ). Мы не знаем какой-либо процедуры, которая могла бы разворачивать и разматывать любую формулу CNF в некоторую равноудаленную формулу DNF, которая не имеет экспоненциального размера. Это был смысл моего предыдущего ответа (пример которого должен был показать экспоненциальный рост, хотя, по общему признанию, такой пример был не лучшим из возможных).$\mathbf{P}$$\mathbf{NP-complete}$

И наоборот, когда вам нужно найти фальсифицирующее назначение, CNF является явным, поскольку он явно показывает вам свои фальсифицирующие назначения (фальсифицируемость CNF принадлежит $\mathbf{P}$ ), в то время как DNF является неявным, так как он скрывает свои фальсифицирующие назначения от ваших глаз (фальсифицируемость DNF) является ). Мы не знаем какой-либо процедуры, которая могла бы разворачивать и разматывать любую формулу DNF в некоторую равносильную формулу CNF, которая не имеет экспоненциального размера.$\mathbf{NP-complete}$

На одном конце у нас есть противоречия, то есть неудовлетворительные формулы. На противоположном конце у нас есть тавтологии, то есть неопределяемые формулы. В середине у нас есть формулы, которые являются как выполнимыми, так и фальсифицируемыми.

В любой формуле CNF с переменными каждое предложение длины k явно кодирует 2 n - k фальсифицирующих присваиваний.$n$$k$$2^{n-k}$

В любой формуле DNF с переменными каждый член длины k явно кодирует 2 n - k, удовлетворяющих присваиваниям.$n$$k$$2^{n-k}$

Формула CNF без предложений - это тавтология, потому что она не имеет фальсифицирующего назначения. Формула CNF, содержащая пустое предложение (которое включает каждое другое предложение), является противоречием, потому что пустое предложение (которое имеет ) указывает, что все 2 $k = 0$$2^n$ присваиваний фальсифицируются. Любая другая формула КНФ является либо Противоречие или один из этих формул в середине (и это , чтобы различать эти 2 случая).$\mathbf{NP-complete}$

Формула DNF без терминов является противоречием, потому что она не имеет удовлетворительного назначения. Формула DNF, содержащая пустой термин (который включает все остальные термины), является тавтологией, потому что пустой термин (который имеет ) указывает, что все 2 $k = 0$$2^n$ назначений удовлетворяют. Любая другая формула ДНФ либо тавтология или один из этих формул в середине (и это , чтобы различать эти 2 случая).$\mathbf{NP-complete}$

$2^n$

$2^n$

В этом свете становится все более очевидным, почему удовлетворенность CNF и фальсифицируемость DNF эквивалентны с точки зрения вычислительной твердости. Потому что на самом деле это одна и та же проблема, поскольку основная задача точно такая же: определить, равно ли объединение нескольких множеств пространству всех возможностей . Такая задача приводит нас к более широкой области подсчета, которая, по моему скромному мнению, является одним из тех путей, которые нужно горячо исследовать, чтобы надеяться на некоторый немаловажный прогресс в решении этих проблем (я сомневаюсь, что дальнейшее исследование решателей на основе резолюций может в конечном итоге принести принципиально новые теоретические достижения, хотя, безусловно, продолжает приносить удивительные практические успехи).

Сложность такой задачи заключается в том, что эти наборы сильно перекрываются друг с другом в режиме включения-исключения.

Наличие такого перекрытия - именно то, где находится точность счета. Более того, тот факт, что мы допускаем перекрытие этих множеств, является той самой причиной, которая позволяет нам иметь компактные формулы, пространство решения которых, тем не менее, экспоненциально велико.

Я решил превратить все эти ответы в этой теме (особенно ответ Джорджо Камерани) в красивую таблицу, чтобы дуальность была видна одним взглядом:

$$\begin{array} {r|c|c} &\text{DNF} & \text{CNF} \\\hline \text{tautology/unfalsifiability} & \textsf{coNP-complete} & \textsf{P} \; \tiny\text{(each clause has a pair of P and ¬P)} \\\hline \text{satisfiability} & \textsf{P} \; \tiny\text{(sat. assignments are explicit)} & \textsf{NP-complete}\\\hline \text{falsifiability} & \textsf{NP-complete} & \textsf{P} \; \tiny\text{(fals. assignments are explicit)} \\\hline \text{unsatisfiability} & \textsf{P} \; \tiny\text{(each clause has a pair of P and ¬P)} & \textsf{coNP-complete} \\\hline \tiny{\text{conversion to normal form, retaining equivalence}} & (*) & (*) \\\hline \tiny{\text{conversion to normal form, retaining satisfiability}} & (**) & \textsf{FP} \\\hline \tiny{\text{conversion to normal form, retaining falsiability}} & \textsf{FP} & (**) \end{array}$$

$(*)$

$(**)$$(*)$$\mathrm{FP}^{\mathrm{NP}[1]}$

Кратчайший ответ на вопрос: показать удовлетворенность (решение SAT) через DNF можно только в экспоненциальном времени в соответствии с таблицей выше.