On Proof Systems for #QBF

Titolo: Sui sistemi di prova per #QBF

Enunciato del problema
Il documento affronta il problema #QBF, che consiste nel calcolare il numero di strategie vincenti per il giocatore esistenziale in una formula booleana quantificata (QBF). Questo problema è identificato come #PSPACE-completo, rendendolo computazionalmente più difficile del analogo problema #SAT (conteggio dei modelli per formule proposizionali), dove il numero di soluzioni è al massimo esponenziale. Al contrario, il numero di strategie vincenti in #QBF può essere doppiamente esponenziale. Sebbene siano stati studiati sistemi di prova per #SAT (ad esempio, KCPS, CPOG, CLIP, MICE) e per QBF (ad esempio, ∀Exp), mancava un sistema di prova dedicato per il problema generale #QBF capace di certificare il conteggio delle strategie vincenti. Esistono solver come d4-QBF e qCounter, ma questi mancano di un framework formalizzato di complessità di prova per la certificazione.

Metodologia
Gli autori estendono i concetti di entrambi i sistemi di prova QBF e i sistemi di prova #SAT per progettare nuovi sistemi di prova per #QBF. Esplorano tre approcci distinti:

1. Sistema Naive: Un sistema rudimentale che elenca tutte le $k$ strategie vincenti. Certifica il conteggio provando la correttezza di ciascuna strategia (tramite prove di tautologia di funzioni di Skolem), provando la distinzione delle strategie (tramite assegnazioni di testimoni) e provando la non esistenza di altre strategie (tramite una codifica di QBF falsa). Gli autori osservano che questo sistema soffre di limiti inferiori banali quando il numero di strategie è doppiamente esponenziale.
2. Sistema basato su espansione (∀Exp+MICE): Questo approccio adatta la regola di $\forall$-espansione utilizzata nella risoluzione QBF. Espande semanticamente la QBF su tutte le possibili assegnazioni alle variabili universali, trasformando il problema #QBF in un problema #SAT. La risultante CNF viene poi elaborata con il sistema di prova #SAT MICE. Gli autori sostengono che questo sistema richiede intrinsecamente una dimensione esponenziale rispetto al numero di variabili universali perché deve espandere tutte le assegnazioni universali per preservare il conteggio dei modelli.
3. Sistema basato su linee (Q-MICE): Il principale contributo è la proposta di Q-MICE (Quantified Model-counting Induction by Claim Extension). Ispirato al sistema MICE per #SAT, Q-MICE è un sistema di prova basato su linee in cui ogni linea è una rivendicazione (claim) della forma $(Q.F, A, c)$.
   • $Q.F$: Una QBF vera.
   • $A$: Una strategia parziale composta da funzioni di Skolem per un sottoinsieme di variabili esistenziali.
   • $c$: Il numero di modi per estendere $A$ in strategie vincenti complete.
   • Regole di inferenza: Q-MICE utilizza tre regole fondamentali:
     • Regola Assiomatica: Deriva rivendicazioni per QBF ristrette in cui la matrice è una tautologia, permettendo il conteggio combinatorio diretto delle estensioni.
     • Regole di Composizione: Permettono di combinare o semplificare le rivendicazioni; Composizione-a somma strategie complete distinte; Composizione-b rimuove le restrizioni sulle strategie quando l'unicità è provata; Composizione-c combina rivendicazioni dove le strategie differiscono solo su specifiche variabili, a condizione che una prova di "assenza di modelli" certifichi che non esistono altre strategie.
     • Regola di Join: Combina due rivendicazioni che differiscono solo per una restrizione su una variabile universale, moltiplicando i loro conteggi, a condizione che la struttura dell'albero di assegnazione lo permetta (grafi a cammino).

Contributi chiave e risultati

• Formalizzazione di Q-MICE: Il documento definisce Q-MICE e ne dimostra la correttezza e la completezza (Teorema 16). È verificabile in tempo polinomiale.
• Separazione Esponenziale: Gli autori dimostrano che Q-MICE è esponenzialmente più forte sia del sistema naive che del sistema ∀Exp+MICE (Teorema 17).
  • Famiglia XOR-PAIRS: Introducono una versione quantificata della formula proposizionale XOR-PAIRS. Mentre questa famiglia richiede prove super-polinomiali (esponenziali) in ∀Exp+MICE a causa della necessità di espandere le variabili universali, Q-MICE fornisce una prova di lunghezza costante e dimensione polinomiale, utilizzando le regole Axiom e Composizione-b.
  • Famiglia Indexed Affine QBF: Costruiscono una famiglia di QBF che rappresenta un semplice processo di cifratura. Questa famiglia ha $2^n$ strategie vincenti, richiedendo prove esponenziali sia nei sistemi naive che in ∀Exp+Mima. Q-MICE gestisce questo caso con una prova di lunghezza lineare e dimensione polinomiale, applicando iterativamente le regole di composizione e join.
• Analisi Strutturale: Il documento evidenzia come i sistemi basati su espansione soffrano di una debolezza strutturale intrinseca (esplosione esponenziale) quando si tratta di variabili universali, mentre Q-MICE intercala la gestione dei quantificatori con il conteggio per mantenere l'efficienza.

Significato e affermazioni
Il documento afferma che l'esistenza di sistemi di prova come Q-MICE è cruciale per far avanzare la teoria di #QBF e per certificare la correttezza dei solver #QBF, un ambito che si trova attualmente nelle sue fasi iniziali. Fornendo un framework per certificare i conteggi dei modelli senza enumerare tutte le strategie, Q-MICE offre una via verso una verifica più robusta dei solver.

Gli autori notano con modestia che, sebbene Q-MICE sia potente, non incorpora ancora le regole di decomposizione presenti in solver allo stato dell'arte come d4-QBF, sebbene suggeriscano che questo potrebbe essere aggiunto come una regola di inferenza modulare. Identificano inoltre problemi aperti, tra cui l'instaurazione di veri limiti inferiori per Q-MICE (congetturando che la formula proposizionale XOR-PAIRS potrebbe essere difficile per esso, sebbene questo non sia ancora un limite inferiore provato) e l'estensione di altri sistemi di prova #SAT (CPOG, CLIP, KCPS) al dominio #QBF. Il documento non propone nuovi solver sperimentali ma si concentra strettamente sulla complessità di prova teorica e sulla separazione di questi sistemi.