Существует ли недетерминированный линейный алгоритм времени для CNF-SAT?

Решение проблемы CNF-SAT можно описать следующим образом:

Вход: булева формула в конъюнктивной нормальной форме. $\phi$

Вопрос: существует ли присвоение переменной, которая удовлетворяет ? $\phi$

Я рассматриваю несколько различных подходов к решению проблемы CNF-SAT с помощью недетерминированной двухленточной машины Тьюринга .

Я считаю, что есть NTM, который решает CNF-SAT в шагах. $n \cdot \texttt{poly}(\log(n))$

Вопрос: существует ли NTM, который решает CNF-SAT за шагов? $O(n)$

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

time-complexity sat turing-machines np nondeterminism Майкл Вехар
источник

Santhanam в 2001 году написал: "SAT NTIME ( polylog )", результат, который следует из фактов, что SAT может быть принят за время polylog в NRAM и что существует эффективное моделирование NRAM НТМ, благодаря Гуревичу и Шелаху ". Так что мне кажется маловероятным, что SAT NTIME ( ) известен. (Ссылка на LNCS 363 от 1989 года.)

\in

$\in$

n

$n$

(n)

$(n)$

n

$n$

(n)

$(n)$

\in

$\in$

n

$n$

Андрас Саламон

@ Босон, предположим, что вам дано не только удовлетворительное задание, но и полное вычисление формулы. Как бы вы проверили, если это правильное вычисление в линейное время? Не ясно даже, что вы можете сделать это для 3CNF-SAT, потому что вам нужно прыгать вокруг, чтобы найти присвоение переменных.

Каве

@Boson Неясно, сможете ли вы проверить, что назначение удовлетворяет формуле за линейное время, с помощью двухмоточной ТМ. Скорее всего, вам придется перемещать головку ленты назад и вперед много раз. Если у вас есть эффективный подход к этой проверке, пожалуйста, дайте мне знать. :)

Майкл Вехар

Просто примечание: если переменные представлены в унарном формате (SAT по-прежнему NPC), то есть NTM с двумя лентами, которая распознает унарную выполнимую формулу вшаги

φ

$\varphi$

2 | φ |

$2|\varphi|$

Марцио де Биаси

@MichaelWehar Если вы используете счетную сортировку, вы можете отсортировать n ключей в диапазоне [0, k] за время O (n + k) в разумной модели произвольного доступа (например, машина Тьюринга с произвольным доступом, где вы можете взять O (log n) время записать индекс, затем можно перейти к этому индексу ленты за 1 шаг). Если вы кодируете каждый литерал как битовую строку (log n + 1), то общее количество предложений и переменных будет не более O (n / log n), и в этом случае O (log n) -временные операции над всеми литералами в порядке. Расширение до двух лент ТМ не так просто, по крайней мере, с учетом сортировки.

Райан Уильямс

Ответы:

Это только расширенный комментарий. Несколько раз назад я спрашивал (сам :-), насколько быстрым может быть многолинейный NTM, который принимает (разумно закодированный) NP-полный язык. Я пришел с этой идеей:

3-SAT остается NP-полной, даже если переменные представлены в унарной форме. В частности, мы можем преобразовать предложение - предположим - произвольной формулы 3-SAT на переменных и предложений в последовательности символов над алфавитом в которой каждое вхождение переменной представляется в унарном виде: $(x_i \lor \neg x_j \lor x_k)$ $\varphi$ $n$ $m$ $\Sigma = \{ +, -, 1 \}$

$+ 1^{i} 0,- 1^{j} ,+ 1^{k}$

Например, можно преобразовать в: $(x_2 \lor -x3 \lor +4)$

+110-1110+11110

Таким образом, мы можем преобразовать формулу 3-SAT в эквивалентную строку объединяющую ее предложения. Язык является NP-полной. $\varphi_i$ $U(\varphi_i)$ $L_U = \{ U(\varphi_i) \mid \varphi_i \in 3-SAT \}$

Двухмоторная НТМ может решить, будет ли строка за время этим способом. $x \in L_U$ $2|x|$

первая головка сканирует ввод слева направо и, следуя внутренней логике, отслеживает вход, выход из предложения или достижение конца формулы. Всякий раз, когда он находит или , вторая голова начинает двигаться вместе с ним на который представляет . В конце , если второй заголовок находится на тогда он угадывает значение истинности или (делает присваивание) и записывает его на вторую ленту; если он находит или тогда этой переменной уже присвоено значение; $+$ $-$ $1^i$ $x_i$ $1^i$ $0$ $+$ $-$ $+$ $-$
в обоих случаях, используя внутреннюю логику, NTM сопоставляет значение истинности под вторым заголовком (назначением) с последним увиденным или ; если они совпадают, то условие удовлетворяется; $+$ $-$
затем вторая голова может вернуться в крайнюю правую ячейку;
с помощью внутренней логики NTM может отслеживать, удовлетворены ли все условия, пока первая головка движется к концу ввода.

Пример:

Tape 1 (formula)    Tape 2 (variable assignments)
+110-1110+11110...  0000000000000...
^                   ^
+110-1110+11110...  0000000000000...
 ^                  ^
+110-1110+11110...  0000000000000...
  ^                  ^
+110-1110+11110...  0+00000000000... first guess set x2=T; matches +
  ^                  ^               so remember that current clause is satisfied
+110-1110+11110...  0+00000000000... 
  ^                  ^
...
+110-1110+11110...  0+00000000000... 
    ^               ^
...
+110-1110+11110...  0++0000000000... second guess set x3=T
       ^              ^              don't reject because current
                                     clause is satisfied (and in every
                                     case another literal must be parsed)

Время может быть сокращено до если мы добавим несколько избыточных символов к представлению предложения: $|x|$

$+ 1^{i} 0^i,- 1^{j} 0^j ,+ 1^{k} 0^k \; ... \; \text{+++}$

( отмечает конец формулы) $\text{+++}$

Таким образом, вторая головка может вернуться в крайнюю левую ячейку, а первая сканирует часть . Используя в качестве разделителя предложений и в качестве маркера конца формулы, мы можем использовать то же представление для формул CNF с произвольным числом литералов в предложении. $0^i$ $\text{++}$ $\text{+++}$

Марцио де Биаси
источник

Унарное представление однозначно, поэтому можно использовать 0/1 для +/-, давая 011011110111110 в качестве первого примера. Затем 00 служит маркером конца предложения, так как 000 не может возникать иначе (если 00 происходит, то это маркер конца переменной и следующий знак, поэтому следующий символ должен быть 1). Сингл worktape содержит угаданной

задание -разрядного к

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

шага для каждого бита ввода.

v

$v$

v

$v$

2

$2$

Андрас Саламон

Другими словами, даже NDTM с односторонней входной лентой и одной рабочей лентой использует не более

шагов для унарного SAT, закодированного с булевым алфавитом.

2 n

$2n$

Саламон

Чтобы сделать вещи еще более аккуратными, можно дополнительно потребовать, чтобы входные данные сначала содержали префикс с числом переменных

заданных в унарном виде. Это позволяет строить догадки при чтении префикса. Тогда это своего рода «унарная кодировка SATLIB», размер которой не более квадратичного в стандартном экземпляре SAT, при условии, что каждая переменная появляется в формуле хотя бы один раз, а переменные пронумерованы от 0 до

. Это, кажется, разумные требования.

v

$v$

v - 1

$v-1$

Андрас Саламон

@ AndrásSalamon: хорошо! Исправляя кодировку и модель (лента с односторонним считыванием + двухсторонняя рабочая лента), мы получаем худшее время выполнения

на входах размера

, где

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

2 n - c

$2n - c$

n

$n$

c

$c$

Марцио Де Биаси

Да, насколько я могу сказать пространственно-временной продукт для одноместной SAT что - то вроде

по стандартному аргументу. Унарное представление переменных позволяет избежать разрыва между самой известнойнижней границей

и прямойверхней границей

для CNF-SAT (хотя лучший алгоритм в этом случае может также уменьшить разрыв).

Θ (n \sqrt{n})

$\Theta(n\sqrt{n})$

Ω (n^{2} / (\log n)^{1 + ε})

$\Omega(n^2/(\log n)^{1+\varepsilon})$

O (n^{3} / (\log n)^{ε^{'}})

$O(n^3/(\log n)^{\varepsilon'})$

Андрас Саламон

Не совсем то, что вы ищете, но для 1-лентного NTM ответ кажется отрицательным: SAT не может быть решен 1-магнитофонным NTM в недетерминированное линейное время.

Согласно этой статье (теорема 4.1), класс регулярных языков - это в точности класс языков, распознаваемых одноленточным NTM за время . Таким образом, если бы существовал одноленточный NTM, решающий SAT во времени , то SAT (точнее, набор выполнимых формул в CNF) был бы регулярным языком, следовательно, разрешимым в детерминированном постоянном пространстве. $REG$ $o(n \log(n))$ $o(n \log(n))$

Бозон
источник

Эта теорема касается только машин Тьюринга с одной головой .

$\:$ (Например, двухголовочные машины Тьюринга могут легко определить язык палиндрома в линейном времени и постоянном пространстве.)

$\;\;\;\;$

Это круто! Большое спасибо. Но меня больше всего интересует двухслойный чехол. :)

Майкл Вехар

Как писал @Ricky. AFAIK все еще согласуется с тем, что мы знаем, что SAT находится в детерминированном линейном времени. Чтобы доказать обратное, вам понадобится нижняя граница суперлинейного времени для SAT, а у нас ее нет (кажется, что она не близка к единице).

Каве