Является ли SAT контекстно-свободным языком?

Я рассматриваю язык всех выполнимых логических формул высказываний, SAT (чтобы гарантировать, что у этого есть конечный алфавит, мы бы закодировали пропозициональные буквы некоторым подходящим способом [править: ответы указали, что ответ на вопрос, возможно, не является устойчивым при различные кодировки, поэтому нужно быть более конкретным - см. мои выводы ниже] ). Мой простой вопрос

Является ли SAT контекстно-свободным языком?

Мое первое предположение состояло в том, что сегодняшний (в начале 2017 года) ответ должен быть «Никто не знает, поскольку это относится к нерешенным вопросам в теории сложности». Однако это не совсем так (см. Ответ ниже), хотя и не полностью ложно. Вот краткое изложение того, что мы знаем (начиная с некоторых очевидных вещей).

SAT не является регулярным (потому что даже синтаксис логики высказываний не является регулярным из-за совпадения скобок)
SAT является контекстно-зависимым (для него нетрудно дать LBA)
SAT является NP-полной (Кук / Левин) и, в частности, определяется недетерминированными ТМ за полиномиальное время.
SAT также может распознаваться однонаправленными недетерминированными стековыми автоматами (1-NSA) (см. Раунды WC, Сложность распознавания в языках среднего уровня , Теория коммутации и автоматов, 1973, 145-158 http://dx.doi.org/ 10.1109 / SWAT.1973.5 )
Слово проблема для контекстно-свободных языков имеет свой собственный класс сложности $\textbf{CFL}$ (см. Https://complexityzoo.uwaterloo.ca/Complexity_Zoo:C#cfl )
, где - класс пространства журнала проблем, сводимый к (см.Https://complexityzoo.uwaterloo.ca/Complexity_Zoo:L#logcfl). Известно, что . $\textbf{CFL}\subseteq\textbf{LOGCFL}\subseteq\textbf{AC}^{\textbf{1}}$ $\textbf{LOGCFL}$ $\textbf{CFL}$ $\textbf{NL}\subseteq\textbf{LOGCFL}$
$\textbf{NL}\subsetneq\textbf{NP}$ $\textbf{NL}=\textbf{NP}$ $\textbf{NC}^{\textbf{1}}\subsetneq\textbf{PH}$ $\textbf{NP}$ $\textbf{LOGCFL}$ $\textbf{LOGCFL}$

Однако этот последний пункт все еще оставляет возможность того, что SAT, как известно, не находится в . В общем, я не мог найти много информации об отношении к иерархии которая могла бы помочь прояснить эпистемологический статус моего вопроса. $\textbf{CFL}$ $\textbf{CFL}$ $\textbf{NC}$

Замечание (после просмотра некоторых первоначальных ответов): я не ожидаю, что формула будет в соединительной нормальной форме (это не будет иметь значения для сути ответа, и обычно аргументы все еще применимы, поскольку CNF также является формулой. Но утверждают, что версия проблемы с постоянным числом переменных является обычной ошибкой, поскольку для синтаксиса нужны скобки.).

Вывод: вопреки моему предположению, основанному на теории сложности, можно прямо показать, что SAT не является контекстно-свободным. Таким образом, ситуация такова:

Известно, что SAT не является контекстно-свободным (другими словами: SAT не находится в ), при условии, что используется «прямое» кодирование формул, где пропозициональные переменные идентифицируются двоичными числами (и некоторые другие символы используются для операторов и разделителей). $\textbf{CFL}$
Не известно, находится ли SAT в , но «большинство экспертов думают», что это не так, поскольку это подразумевает . Это также означает, что неизвестно, являются ли другие «разумные» кодировки SAT контекстно-свободными (при условии, что мы считаем логическое пространство приемлемым усилием кодирования для NP-трудной задачи). $\textbf{LOGCFL}$ $\textbf{P}=\textbf{NP}$

Обратите внимание, что эти две точки не подразумевают . Это можно показать непосредственно, показав, что в есть языки (следовательно, в ), которые не являются контекстно-свободными (например, ). $\textbf{CFL}\subsetneq\textbf{LOGCFL}$ $\textbf{L}$ $\textbf{LOGCFL}$ $a^nb^nc^n$

cc.complexity-theory circuit-complexity sat context-free MAK
источник

Если бы это было так, то P = NP.

Райан

Если бы SAT были свободны от контекста, то динамическое программирование (алгоритм CYK) давало бы алгоритм полиномиального времени для проверки членства в SAT, давая P = NP. Даже P = NP не означает, что SAT не зависят от контекста. Такое кодирование переменных кажется более важным, чем вы полагаете. Я не проработал детали, но если бы вы добавили к переменным унарные или двоичные «индексы», я думаю, у вас будут проблемы с различием (x и y) от (x и не x) для достаточно больших индексов.

AdamF

Вы должны быть точными в отношении представления, прежде чем претендовать на выводы P = NP. Например, факторинг числа N является полиномиальным временем в N (интересный вопрос касается количества битов, необходимых для записи N в двоичном виде, или о log N).

Арье

Я знал о заключении P = NP, и поэтому не ожидалось, что ответом будет «да» (извините за то, что я немного провокационен в том, как я это сформулировал ;-). Я все еще задавался вопросом, действительно ли это известно или просто то, во что «верит большинство экспертов» (ответы теперь ясно указывают на то, что первое верно; я выберу один в свое время).

мак

Ответы:

Просто альтернативное доказательство, использующее сочетание хорошо известных результатов.

Предположим, что:

переменные выражаются с помощью регулярного выражения $d = (+|-)1(0|1)^*$
и что ( обычный ) язык (над используемый для представления формул CNF, имеет вид: ; только отметьте, что захватывает все допустимые формулы CNF вплоть до переименования переменных. $\Sigma = \{0,1,+,-,\land,\lor\})$ $S = \{ d^+ (\lor d^+)^*(\land (d^+ (\lor d^+)^*))^* \}$ $S$

Например, записывается в виде: ( оператор имеет приоритет над ) , $\varphi = (x_1 \lor x_2) \land -x_3$ $s_{\varphi} = +1 \lor +10 \land -11 \in S$ $\lor$ $\land$

Предположим, что st, соответствующая формула выполнима есть CF. $L = \{ s_{\varphi} \in S \, \mid$ $\varphi$ $\}$

Если мы пересекаем его с обычным языком: мы все равно получаем язык CF. Мы также можем применить гомоморфизм: , и язык остается CF. $R = \{ +1^a \land -1^b \land -1^c \mid a,b,c > 0 \}$ $h(+) = \epsilon$ $h(-) = \epsilon$

Но мы получаем следующий язык: , потому что если то формула "source" что неудовлетворительно (аналогично, если ). Но является хорошо известным противоречием языка CF . $L' = \{ 1^a \land 1^b \land 1^c \mid a \neq b, a \neq c\}$ $a=b$ $+x_a \land -x_a \land -x_b$ $a=c$ $L'$ $\Rightarrow$

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

Я принял этот ответ сейчас, так как с другим подходом все еще остается открытым вопрос (см. Комментарии), и мне нравится несколько более базовый аргумент. Было бы неплохо подчеркнуть, что аргумент специфичен для выбранной кодировки, и действительно неизвестно, можно ли найти другую простую (logspace) кодировку, которая приводит к контекстно-свободному языку.

Мак

@mak: Я подозреваю, что любое другое «разумное» кодирование SAT может быть доказано не CF с подобной техникой. Возможно, другим интересным направлением было бы изучение того, можем ли мы применить какую-то диагонализацию для получения более общего доказательства: формула SAT кодирует вычисление, которое имитирует автоматы нажатия на заданном входе, и оно выполнимо тогда и только тогда, когда это не так. Я не принимаю это. Но это только нечеткая идея ...

Марцио Де

Проверка, находится ли строка на обычном языке в P. Предположим, что SAT был в Reg. Тогда NP = coNP. Пусть L будет в Reg. Рассмотрим формулу, которая верна, если ее нет в L. Она находится в NP, поэтому ее можно выразить в виде формулы SAT. Это на языке, если это не так.

Каве

Если число переменных конечно, то так же, как и число выполнимых конъюнкций, ваш язык SAT конечен (и, следовательно, регулярен). [Редактировать: это утверждение принимает форму CNFSAT.]

В противном случае, давайте согласимся кодировать формулы, такие как , в . Мы будем использовать лемму Огдена, чтобы доказать, что язык всех выполнимых конъюнкций не является контекстно-свободным. $(x_{17}\vee \neg x_{21})\wedge (x_{1}\vee x_{2}\vee x_3)$ $(17+\tilde{} 21)(1+2+3)$

Пусть будет «маркирующей» константой в лемме Огдена и рассмотрим sat-формулу , первое предложение которой состоит из - то есть кодировки , где - десятичное число, состоящее из из них. Мы отмечаем единиц из а затем требуем, чтобы все накачки соответствующего разложения (см. Заключение леммы Огдена) также были выполнимыми. Но мы можем легко заблокировать это, требуя, чтобы ни одно предложение, содержащее , где - последовательность , короче чем $p$ $w$ $(1^p)$ $(x_N)$ $N$ $p$ $p$ $1^p$ $w$ $x_q$ $q$ $1$ $p$ быть выполнимым - например, гарантируя, что каждое другое предложение имеет отрицание каждого такого . Это означает, что не имеет свойства «отрицательной накачки», и мы заключаем, что язык не является контекстно-свободным. [Примечание: я проигнорировал тривиальные случаи, когда накачка производит плохо сформированные струны.] $w$ $x_q$ $w$

Арье
источник

Примечание: в моем утверждении, что для конечного числа переменных язык конечен, я неявно запрещаю повторять переменную в предложении или предложении неограниченно много раз

Aryeh

... Но я думаю, что язык все еще регулярен, потому что кто-то берет конечный набор формул "по существу различных" (т.е. без тривиальных повторений), а затем допускает различные повторения.

Арье

Претензия с регулярностью работает только для CNFSAT (я добавил пояснение к своему вопросу).

мак

Даже с произвольными формулами, не относящимися к CNF, в конечном числе переменных, выполнимость (и любой язык, который не может различить две логически эквивалентные формулы по этому вопросу) легко увидеть как контекстно-свободную. Однако я не вижу актуальности этого. Удовлетворенность формул в конечном числе переменных является тривиальной проблемой, которая не имеет ничего общего со сложностью SAT.

Эмиль Йержабек

Хорошо, я вижу проблему - я неявно предполагал, чтоможет быть ограничен по длине (как в классической лемме прокачки), но также может указывать что-то о его расположении в строке. Я думаю, что аргумент можно исправить, заново выполнив лемму прокачки с нуля. Мы сделаем эту первую переменную действительно длинной последовательностью 1 - достаточно длинной, чтобы какое-то поддерево, генерирующее непрерывную подстроку из этих 1, было достаточно глубоким для применения принципа pidgeonhole.

| x y z |

$|xyz|$

Арье