Как 2-CNF SAT находится в P, в то время как 3-CNF SAT находится в NPC? - PullRequest
6 голосов
/ 12 декабря 2011

Я действительно смущен, почему 2-CNF SAT находится в P, в то время как 3-CNF SAT находится в NPC.Я читаю CLRS, и я понимаю, как они доказывают, что 3-CNF SAT находится в NPC.Разве я не могу использовать ту же сводимость от SAT к 2-CNF-SAT, чтобы доказать, что 2-CNF-SAT есть в NPC.Я не понимаю, почему 2-CNF SAT находится в P.

Ответы [ 2 ]

13 голосов
/ 12 декабря 2011

почему 2-CNF SAT находится в P

Потому что есть полиномиальный алгоритм для его решения.

Черновой набросок доказательства:

Обратите внимание, что любое предложение в 2-CNF имеет вид A => B, где A и B являются либо переменными, либо их отрицанием. Следовательно, мы можем сказать, что в этом пункте говорится, что когда A истинно, это заставляет B быть истинным. Это также означает, что B ложно заставляет A быть ложным. Мы должны рассмотреть это позже.

Теперь, вы можете взять переменную одну за другой и найти, если она транзитивно заставляет себя быть ее отрицательной (A => B => C => ... => non A) и наоборот (не A) => ... => А). Если первое верно, A должно быть ложным; если второе, А это правда. Если оба, формула неудовлетворительная.

Если вы не найдете ни одной переменной, которая делает формулу неудовлетворительной, она выполнима.

Обратите внимание, что этот "брутальный" алгоритм не является реальным алгоритмом, использующим сильно связанные компоненты графа, о котором я рекомендую вам прочитать. Тем не менее, он является полиномиальным (поиск одной переменной явно O (N ^ 2), так как вы заставляете одну переменную за раз, учитывая O (N) предложения, и вы рассматриваете O (N) переменных, что означает, что алгоритм является полиномиальным) , Обратите внимание, что тот факт, что в предложении содержится не более двух литералов, имеет решающее значение. Если бы пункты были A => B or C или что-то еще, это не сработало бы так хорошо.

3 голосов
/ 12 декабря 2011

Каноническое сокращение от CNF SAT до 3-CNF SAT состоит в том, чтобы взять условие типа lit_1 ИЛИ lit_2 ИЛИ ... ИЛИ lit_n и заменить его двумя предложениями lit_1 ИЛИ lit_2 ИЛИ ... ИЛИ lit_ {этаж (н / 2)} ИЛИ var, lit_ {floor (n / 2) + 1} ИЛИ ... ИЛИ lit_n ИЛИ НЕ var.Если вы попытаетесь разорвать предложение с тремя литералами таким образом, вы получите еще одно предложение с тремя литералами, поэтому такое же доказательство не будет работать для 2-CNF SAT (и, вероятно, по уважительной причине).

...