Универсальные кванторы в QBF

Question

Я искал сокращения в / из языка TQBF и мне удалось застрять на чем-то, что почти наверняка не соответствует действительности (или, если это правда, мне не хватает значительных вычислительных затрат, связанных с этим) в отношении упрощения Экземпляры TQBF.

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

$\exists a \forall b \exists c \forall d$ $\psi(a,b,c,d)$

$\psi(a,b,c,d) = (\neg a \vee b \vee c)\wedge (\neg b \vee \neg c \vee d)\wedge (a \vee c \vee \neg d)$

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

$\exists a \exists c$ $\phi(a,c)$,

$\phi (a,c) = (\neg a \vee c)\wedge (\neg c) \wedge (a \vee c)$

что явно невыполнимо. Если вместо этого примера мы посмотрим на это:

$\exists a \forall b \exists c \forall d$ $\psi(a,b,c,d)$

$\psi(a,b,c,d) = (\neg a \vee b \vee \neg c)\wedge (\neg b \vee c \vee d)\wedge (a \vee c \vee \neg d)$

который явно является выполнимым (установите c в значение true, a в значение false) и который имеет "ядро"

$\exists a \exists c$ $\phi(a,c)$,

$\phi (a,c) = (\neg a \vee \neg c)\wedge (c) \wedge (a \vee c)$

это также выполнимо с теми же настройками переменных.

Если этот метод всегда работает, это может означать, что существует линейное во времени сокращение от TQBF до SAT количества универсальных кванторов и количества вхождений универсально количественно определенных переменных в формуле, показывая, что TQBF является NP-Complete (он уже известен как PSPACE-Complete и, следовательно, NP-Hard, поэтому, если он находится в NP, это NP-Complete) и, кроме того, что NP = PSPACE. Я был бы совершенно ошеломлен, если бы это было так, но мне не удалось найти контрпример (или отсутствующие вычислительные затраты при сокращении, которые делают его не полиномиальным). Что мне не хватает?

Answer 1

Ваша интуиция была правильной. Не работает. Вот контрпример.

Рассмотреть возможность $\forall a \exists b \varphi(a,b)$ где $\varphi(a,b) = (a \lor \neg b) \land (\neg a \lor b)$. Это утверждение истинно.

Однако, если мы удалим $a$ следуя вашей процедуре, мы получаем $\exists b \psi(b)$ где $\psi(b) = ((\neg b) \land (b))$; и это утверждение считается ложным.

Один из способов понять, почему ваш метод не работает, - это $\forall a \exists b \varphi(a,b)$ не эквивалентно $\exists b \forall a \varphi(a,b)$. В лучшем случае ваш метод может работать, если все$\forall$находятся внутри, т. е. для предложения формы $\exists \cdots \exists \forall \cdots \forall$, но не для любого другого образца $\exists$ а также $\forall$.