A Resolution-Based Interactive Proof System for UNSAT

1. Il Problema

Il lavoro affronta il problema fondamentale dell'asimmetria tra la verifica delle certificazioni SAT (soddisfacibilità) e UNSAT (insoddisfacibilità) nei moderni risolutori di formule booleane (SAT/QBF).

• Certificati SAT: Una assegnazione soddisfacente può essere verificata in tempo polinomiale (o lineare) rispetto alla dimensione della formula.
• Certificati UNSAT: Le prove di insoddisfacibilità (come le dimostrazioni per risoluzione o i certificati DRAT) possono avere una dimensione esponenziale nel caso peggiore. Sebbene la verifica sia lineare rispetto alla dimensione del certificato, la dimensione stessa del certificato può raggiungere terabyte, rendendo impossibile la verifica da parte di client con risorse limitate in scenari di calcolo distribuito (es. un client invia una formula a un server potente e riceve indietro una prova).

L'obiettivo è sviluppare un sistema di certificazione interattiva basato sul teorema $IP = PSPACE$, dove il Verificatore (client) impiega solo tempo polinomiale nella dimensione della formula originale, indipendentemente dalla dimensione esponenziale della prova, mentre il Provocatore (server) esegue un algoritmo risolutivo. La sfida principale è rendere questi protocolli competitivi rispetto ad algoritmi di risoluzione pratici (non solo brute-force), limitando l'overhead computazionale del Provocatore.

2. Metodologia

Gli autori propongono un framework teorico e pratico per costruire protocolli interattivi competitivi basati su algoritmi di risoluzione.

A. Riduzione a Arithmetizzazione

Il cuore della metodologia è una riduzione del problema di trovare un protocollo competitivo alla ricerca di un'arithmetizzazione (mappatura di formule booleane in polinomi su un campo finito) che soddisfi specifiche proprietà di commutatività.

• Un algoritmo per UNSAT è visto come una sequenza di "macro-step" che trasformano una formula $\phi_0$ in $\phi_k$ (equivalente a falso se UNSAT).
• L'arithmetizzazione $A$ mappa ogni formula in un polinomio.
• Per essere compatibile con un macro-step $M$, deve esistere un'operazione sui polinomi $P_M$ tale che il diagramma commuti: applicare $M$ alla formula e poi arithmetizzare deve dare lo stesso risultato che arithmetizzare la formula e poi applicare $P_M$.
• Inoltre, $P_M$ deve commutare con le valutazioni parziali (assegnazioni parziali di variabili).

B. L'Algoritmo Target: Davis-Putnam

Gli autori applicano questa metodologia alla procedura di risoluzione Davis-Putnam (una versione semplificata basata sulla risoluzione completa rispetto a una variabile e pulizia delle clausole).

• Dimostrano che le arithmetizzazioni standard (es. quelle usate nei teoremi classici IP=PSPACE) non sono compatibili con la procedura di Davis-Putnam a causa della natura delle operazioni di risoluzione e pulizia.
• Introducono una arithmetizzazione non standard, chiamata $B$, definita ricorsivamente:
  • $B(x) = 1-x$
  • $B(\neg x) = x^3$
  • $B(\phi_1 \land \phi_2) = B(\phi_1) + B(\phi_2)$
  • $B(\phi_1 \lor \phi_2) = B(\phi_1) \cdot B(\phi_2)$
• Questa scelta specifica (in particolare l'uso di $x^3$ per le negazioni) permette di definire operazioni polinomiali ($\gamma_x$ e $\delta_x$) che simulano correttamente i passi di risoluzione ($R_x$) e pulizia ($C_x$) mantenendo le proprietà di commutatività richieste.

C. Il Protocollo Interattivo

Il protocollo funziona come segue:

1. Il Provocatore esegue l'algoritmo Davis-Putnam, calcolando la sequenza di formule $\phi_0, \dots, \phi_k$.
2. Invece di inviare la prova completa, il Provocatore e il Verificatore interagiscono su un campo finito $\mathbb{F}_q$.
3. Il Verificatore sceglie assegnazioni casuali per le variabili. Il Provocatore invia i valori dei polinomi arithmetizzati corrispondenti.
4. Il Verificatore verifica la coerenza tra i passi usando il Lemma di Schwartz-Zippel: se il Provocatore mente su un passaggio, la probabilità che il valore casuale scelto dal Verificatore "nasconda" l'errore è trascurabile.
5. Il Verificatore esegue solo calcoli polinomiali sulla formula originale, senza mai leggere la prova esponenziale.

3. Contributi Chiave

1. Teorema di Riduzione: Dimostrazione che la ricerca di protocolli interattivi competitivi per un algoritmo di UNSAT si riduce alla ricerca di un'arithmetizzazione compatibile con i macro-step di quell'algoritmo.
2. Primo Protocollo per Davis-Putnam: Presentazione del primo protocollo interattivo competitivo per la procedura di Davis-Putnam, basato su un'arithmetizzazione non standard ($B$).
3. Implementazione (icdp): Sviluppo di uno strumento chiamato icdp (Interactively Certified Davis-Putnam) che implementa sia il Provocatore che il Verificatore.
4. Analisi Sperimentale: Confronto empirico tra certificazione interattiva e certificazione convenzionale (basata su prove di risoluzione e DRAT).

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su un set di 108 istanze insoddisfacibili (problemi combinatori come il principio delle casse, colorazione di grafi, ecc.).

• Tempo del Provocatore: Il Provocatore nel setting interattivo è più lento rispetto all'esecuzione standard di Davis-Putnam, ma l'overhead è quasi costante (fattore polinomiale basso). Tuttavia, Davis-Putnam è intrinsecamente lento rispetto ai moderni risolutori CDCL (come Kissat).
• Tempo del Verificatore: Il Verificatore interattivo è ordini di grandezza più veloce (circa 10 volte più veloce) rispetto ai verificatori convenzionali (come DRAT-trim) che devono leggere e processare prove massive.
• Complessità di Comunicazione: Questo è il risultato più significativo.
  • Le prove convenzionali (DRAT/Resolution) possono essere enormi (centinaia di MiB o TiB).
  • La comunicazione nel protocollo interattivo è estremamente ridotta. I dati mostrano che la dimensione dei dati scambiati cresce come una potenza molto bassa (circa $x^{0.2}$) rispetto alla dimensione della prova convenzionale.
  • In scenari ipotetici con prove di petabyte, il Provocatore dovrebbe inviare al Verificatore solo pochi kilobyte.
• Confronto con IP=PSPACE generico: I protocolli generici basati su IP=PSPACE richiederebbero al Provocatore di generare tabelle di verità complete (tempo esponenziale nel numero di variabili), rendendoli inutilizzabili. Il protocollo proposto, essendo competitivo con un algoritmo di risoluzione, gestisce istanze con più di 50 variabili, superando i limiti dei protocolli generici.

5. Significato e Conclusioni

• Validazione Teorica: Il lavoro dimostra che è possibile ottenere certificazioni interattive efficienti non solo per algoritmi di forza bruta, ma anche per algoritmi di risoluzione strutturati, superando la barriera della commutatività tramite arithmetizzazioni non standard.
• Implicazioni Pratiche: Sebbene Davis-Putnam non sia più lo stato dell'arte (i moderni solver usano CDCL), il successo su questo algoritmo apre la strada a protocolli competitivi per algoritmi più moderni.
• Scalabilità: Il sistema offre una soluzione promettente per servizi di SAT-solving distribuiti, dove un client con risorse limitate può delegare la risoluzione a un server potente ottenendo una prova verificabile in tempo polinomiale e con comunicazione minima.
• Sfide Future: La sfida principale rimane estendere queste tecniche a algoritmi moderni come CDCL, che utilizzano apprendimento di clausole e backtracking non deterministico, molto più complessi della risoluzione pura di Davis-Putnam.

In sintesi, il paper fornisce un ponte teorico e pratico tra la complessità computazionale interattiva e la risoluzione pratica delle formule booleane, dimostrando che la verifica di insoddisfacibilità può essere resa efficiente per il verificatore senza richiedere prove esponenziali, a patto di utilizzare arithmetizzazioni creative.