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

22

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

Кава
источник
5
Не все решатели ограничений используют CNF в качестве входных данных. Некоторые предпочитают этого не делать, потому что структура исходного набора ограничений сохраняется.
Дэйв Кларк
1
этот вопрос имеет ошибочную предпосылку и не думаю, что он заслуживает такой высокой оценки, как в настоящее время сформулировано. SAT определяется как решение формул CNF. Существует проблема решения DNF (вы могли бы даже назвать это нахождением удовлетворительных назначений), но это не называется / прозвище SAT в CS. & imho это должно быть перенесено в cs.se ... еще одно примечание - преобразование CNF в DNF и наоборот на самом деле очень похоже или может рассматриваться как алгоритм сжатия, который в некоторых случаях дает сбой (приводящий к экспоненциальному увеличению) в размере)
взн
10
@vzn: на самом деле, «SAT» иногда используется для обозначения проблемы поиска удовлетворительного назначения для любой логической формулы. CNF-SAT является просто наиболее интересным частным случаем, поэтому мы склонны использовать «SAT» для обозначения CNF-SAT, в частности, как своего рода синехдоха. DNF-SAT, конечно, эффективно разрешима, так же, как CNF-TAUTOLOGY эффективно разрешима. Вопрос, похоже, основан на неосознании этого.
Ниль де Бодрап,

Ответы:

56

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

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

Jeffε
источник
afaik преобразование DNF в CNF и наоборот не совсем то же самое, что и P против NP, хотя, вероятно, оно относится к некоторым важным разделениям классов сложности (очевидно, для классов «больше», чем NP) ... проблема в том, что это может привести к экспоненциальный рост по размеру ... и в любом случае преобразование между CNF и DNF не является проблемой решения ... есть несколько способов превратить это в проблему решения ...
vzn
10
Я думаю, что Джефф был в том, что DNF-SAT находится в P, поэтому он не может быть NP-полным, если P = NP.
Люк Мэтисон
2
«все известные преобразования» неверны, учитывая текущие знания, на самом деле, существуют DNF <=> формулы / преобразования CNF, которые доказуемо требуют экспоненциального увеличения пространства вне зависимости от алгоритма ... думаю, это показалось, что обсуждение преобразования CNF <=> DNF было весьма актуальным на этот вопрос и этот ответ намекает на это ... используется ли аббревиатура "DNF-SAT" в литературе? не вспоминаю, что видел это сам ... мне кажется, что это смущает меня ... Удовлетворение DNF - это проблема решения, конверсия DNF <-> CNF - это функциональная проблема, и ответ не делает это различие слишком ясным; отличный ответ был бы ...
vzn
@ Jɛ ff E: Вы не возражаете уточнить, что вы имели в виду под «произвольной логической формулой» здесь? Глядя на статью Карпа , стр. 92, СООТВЕТСТВИЕ определяется по формулам CNF. Это не влияет на ваш ответ на вопрос OP, но я пытаюсь убедиться, что нет более общих результатов для произвольных логических формул (то есть формул, которые не обязательно находятся в CNF). Спасибо
Lyes
22

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

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

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

Миколас
источник
1
Хорошая ссылка: soe.ucsc.edu/classes/cmps132/Winter05/hw/hw8sols.pdf
MS Dousti
1
@TayfunPay они делают. Например, . Если вы запрещаете предложения, содержащие одну и ту же переменную дважды, то существует единственное представление тавтологии, которое представляет собой пустой набор предложений. {{¬xx}}
Миколас
3
@Tayfun, хотя я согласен с тем, что определения, как правило, запрещают повторяющиеся переменные в предложениях, я не думаю, что когда-либо видел определение, которое запрещало бы пустой набор предложений. (И мне непонятно, почему вы хотели бы это сделать)
Миколас
2
@Tayfun 1) не могли бы вы указать мне на публикацию, в которой говорится, что в CNF нет тавтологий или что пустой набор предложений не является CNF? 2) если вы запрещаете пустой набор предложений, то вам также следует запретить пустое предложение, и вы также не можете представлять false 3) если вы не разрешаете true и / или false в CNF, вы теряете свойство представлять все булевы функции, зачем вам это делать?
Миколас
1
«не должно быть ни повторения переменных, ни литералов ни в одном данном предложении». --- это не запрещает пустые формулы или предложения. Кстати, если вы запретите пустое предложение, вы больше не сможете делать доказательства опровержения резолюции, которые составляют довольно важную часть автоматизированного рассуждения.
Миколас
18

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

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

Лев Рейзин
источник
11

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


По сути, формула DNF является дизъюнкцией пунктов , где каждый пункт c i = l i , 1. , , л я , к является конъюнкция литералов. Давайте называть положение с я конфликтующим тогда и только тогда , когда оно содержит как буквальный л и его отрицание ¬ л . Легко видеть, что каждое неконфликтующее предложение просто кодирует 2 n - kс1,,,смci=li,1...li,kcil¬l2nkРешения формулы. Таким образом, весь DNF - это просто перечень решений. Формула может иметь экспоненциально много решений, поэтому соответствующая формула DNF может иметь экспоненциально много предложений. Попробуйте преобразовать эту формулу CNF:

l1l2l3l4

l5l6l7l8

l9l10l11l12

l13l14l15l16

l17l18l19l20

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

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

Джорджо Камерани
источник
4
Чтобы получить правильное форматирование LaTeX, замените \ and и \ или на \ land и \ lor (или \ wedge and \ vee).
Джефф
2
По сути, нет ничего более компактного в преобразовании в обычный CNF, реальный ключ к вопросу OP заключается в том, что вы можете создавать эти «равноудаленные» функции CNF со вспомогательными переменными. Вероятно, есть аналогичное приближение, которое вы можете сделать с DNF, чтобы решить другую проблему, вместо того, чтобы проверять на удовлетворенность. (равностепенную невыполнимости функции ...?)
dividebyzero
1
Это понимание Джорджо Камерани не очень хорошее. Такое же экспоненциальное увеличение количества предложений может произойти, если вы конвертируете что-то в CNF. Выберите этот же пример и замените "и" на "или" s. Преобразование из этого маленького выражения DNF в CNF будет таким же огромным. У них есть отношения инь-и-янь к ним.
Divybyzero
@dividebyzero: Я посвятил отдельный ответ на ваши комментарии.
Джорджио Камерани,
6

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

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

Миколас
источник
4

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

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

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

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

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

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

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

Формула CNF без предложений - это тавтология, потому что она не имеет фальсифицирующего назначения. Формула CNF, содержащая пустое предложение (которое включает каждое другое предложение), является противоречием, потому что пустое предложение (которое имеет ) указывает, что все 2 nКзнак равно02N присваиваний фальсифицируются. Любая другая формула КНФ является либо Противоречие или один из этих формул в середине (и это , чтобы различать эти 2 случая).NPcomplete

Формула DNF без терминов является противоречием, потому что она не имеет удовлетворительного назначения. Формула DNF, содержащая пустой термин (который включает все остальные термины), является тавтологией, потому что пустой термин (который имеет ) указывает, что все 2 nk=02n назначений удовлетворяют. Любая другая формула ДНФ либо тавтология или один из этих формул в середине (и это , чтобы различать эти 2 случая).NPcompletе

2N

2N

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

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

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

Джорджо Камерани
источник
4

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

DNFCNFтавтология / unfalsifiabilityCONP-полнойп(в каждом пункте есть пара P и ¬P)выполнимостип(сб. назначения явные)NP-полнойфальсифицируемостьNP-полнойп(фальш. назначения явные)невыполнимостип(в каждом пункте есть пара P и ¬P)CONP-полнойпреобразование в нормальную форму с сохранением эквивалентности(*)(*)перевод в нормальную форму с сохранением выполнимости(**)FPпреобразование в нормальную форму с сохранением фальсификацииFP(**)

(*)

(**)(*)FпNп[1]

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

mcb
источник
1
Что такое «формула PL» и что означает «NF»?
Джошуа Грохов
4
Здесь есть несколько вопросов. (1) Я думаю, что под «неутолимостью» вы подразумеваете «тавтологию». (2) KNF должен быть CNF.
Гек Беннетт
2
До сих пор не ясно, что вы подразумеваете под «NF (сохранить удовлетворяемость)». Означает ли это, что алгоритм А такой, чтоA(φ) выполнимо, если φ есть, но если φ то неудовлетворительно A(φ) может быть и тем более для всех выполнимых формул φ, A(φ)имеет такой же выход? Это то, что я думаю из вашей записи, но эта проблема не будет в P для CNF. Так что ты имеешь в виду?
Джошуа Грохов
1
(1) «логика предикатов» должна быть «логикой высказываний». (2) Преобразования в нормальные формы - это не проблемы решения, а функциональные проблемы (или, скорее, проблемы поиска, поскольку «нормальные формы» не являются уникальными). Итак, приведенные в таблице классы решений неуместны.
Эмиль Йержабек поддерживает Монику
1
Что Δ3п там делаешь?
Эмиль Йержабек поддерживает Монику