Formula booleana quantificata
Una formula booleana quantificata (o QBF, dall'inglese quantified Boolean formula) è una formula della logica proposizionale con quantificatori (nota anche come logica proposizionale del secondo ordine) in cui ogni variabile è quantificata (o vincolataa, bound) tramite un quantificatore esistenziale o universale all'inizio della formula. Il problema di verificare una QBF sia vera (ovvero che appartenga al linguaggio delle true QBF, o TQBF) è noto come QSAT (quantified SAT).
Soddisfacibilità
modificaNella teoria della complessità computazionale, il problema QSAT è una generalizzazione della soddisfacibilità booleana (SAT) in cui si assume che ciascuna variabile sia quantificata esistenzialmente o universalemente. Il problema consiste nel verificare se una data QBF sia vera o falsa. Ad esempio, data la formula seguente:
si vuole verificare se per ogni assegnazione della variabile esiste un'assegnazione delle variabili e tale che la formula possa essere valutata vera. Si noti che, dato che nessuna variabile è libera, tali formule sono logicamente equivalenti a vero o falso.
QBF è il problema completo canonico per PSPACE, la classe di complessità dei problemi risolvibili da una macchina di Turing (deterministica o non) in spazio polinomiale.[1] Data una QBF in forma di albero sintattico astratto, il problema può essere risolto facilmente trammite un insieme di procedure mutualmente ricorsive che eseguono la valutazione della formula. Tale algoritmo usa uno spazio proporzionale all'altezza dell'albero, che è lineare nel caso peggiore, ma usa tempo esponenziale rispetto al numero di quantificatori.
Se il contenimento della classe di complessità MA in PSPACE fosse stretto, cosa largamente creduta vera, allora QSAT non può essere risolto, né una sua soluzione può essere verificata, da una macchina di Turing probabilistica e deterministica in tempo polinomiale. Può comunque essere risolto da una macchina di Turing alternante in tempo lineare, dal momento che AP = PSPACE.[2]
L'equivalenza IP = PSPACE venne dimostrata tramite un sistema di prova interattivo in grado di risolvere una particolare aritmetizzazione di QSAT.[3]
Note
modifica- ^ (EN) M. Garey e D. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, San Francisco, California, 1979, ISBN 0-7167-1045-5.
- ^ (EN) A. Chandra, D. Kozen, and L. Stockmeyer, Alternation, in Journal of the ACM, vol. 28, n. 1, 1981, pp. 114–133, DOI:10.1145/322234.322243.
- ^ (EN) Adi Shamir, Ip = Pspace, in Journal of the ACM, vol. 39, n. 4, 1992, pp. 869–877, DOI:10.1145/146585.146609.
