Quantificatori universali in QBF
Ho esaminato le riduzioni al / dal linguaggio TQBF e sono riuscito a rimanere bloccato su qualcosa che quasi certamente non è vero (o, se è vero, mi manca un costo computazionale significativo ad esso associato) rispetto alla semplificazione Istanze TQBF.
Per semplicità, limitiamo l'attenzione alle istanze TQBF in forma normale prenex e CNF senza variabili libere. La mia ipotesi (che sospetto fortemente sia sbagliata, ma non sono riuscito a trovare un controesempio) è che un tale TQBF sia soddisfacente se e solo se il TQBF che risulta dalla rimozione di tutte le istanze di variabili quantificate universalmente dalla frase è soddisfacente. Ad esempio, prendi il seguente esempio:
$\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)$
In primo luogo, sostengo che questa istanza non è soddisfacente (facilmente verificabile a mano). Se applichiamo il metodo descritto sopra, otteniamo il seguente "core":
$\exists a \exists c$ $\phi(a,c)$,
$\phi (a,c) = (\neg a \vee c)\wedge (\neg c) \wedge (a \vee c)$
che chiaramente non è soddisfacente. Se invece di questo esempio guardiamo questo:
$\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)$
che è chiaramente soddisfacente (imposta c a true, a a false) e che ha un "nucleo" di
$\exists a \exists c$ $\phi(a,c)$,
$\phi (a,c) = (\neg a \vee \neg c)\wedge (c) \wedge (a \vee c)$
anche questo è soddisfacente con le stesse impostazioni delle variabili.
Se questo metodo funziona sempre, ciò sembrerebbe implicare che c'è una riduzione da TQBF a SAT nel tempo lineare nel numero di quantificatori universali e nel numero di occorrenze delle variabili quantificate universalmente nella formula, dimostrando che TQBF è NP-Completo (è già noto per essere PSPACE-Complete e quindi NP-Hard, quindi se è in NP è NP-Complete) e inoltre NP = PSPACE. Sarei completamente sbalordito se fosse così, ma non sono riuscito a trovare un controesempio (o un costo computazionale mancante nella riduzione che lo rende un tempo non polinomiale). Cosa mi sto perdendo?
Risposte
La tua intuizione era giusta. Non funziona. Ecco un controesempio.
Tenere conto $\forall a \exists b \varphi(a,b)$ dove $\varphi(a,b) = (a \lor \neg b) \land (\neg a \lor b)$. Questa affermazione restituisce vero.
Tuttavia, se rimuoviamo $a$ seguendo la tua procedura, otteniamo $\exists b \psi(b)$ dove $\psi(b) = ((\neg b) \land (b))$; e quell'affermazione viene valutata come falsa.
Un modo per capire perché il tuo metodo non funziona è quello $\forall a \exists b \varphi(a,b)$ non è equivalente a $\exists b \forall a \varphi(a,b)$. Al massimo il tuo metodo potrebbe funzionare se tutti i file$\forall$sono all'interno, cioè per una frase del modulo $\exists \cdots \exists \forall \cdots \forall$, ma non per qualsiasi altro modello di $\exists$ e $\forall$.