Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols

Titolo

Certificazione Induttiva della Soddisfacibilità per Quantificatori Universali e Simboli Funzionali Non Interpretati

1. Il Problema

Il lavoro affronta una sfida fondamentale nel ragionamento automatizzato e nei solver SMT (Satisfiability Modulo Theories): la determinazione della soddisfacibilità di formule che combinano quantificatori universali e simboli funzionali non interpretati (spesso usati per modellare array).

• Contesto: La combinazione di questi elementi, nota come logica UFLIA (Uninterpreted Functions and Linear Integer Arithmetic), è in generale indecidibile.
• Limiti degli approcci attuali: I solver SMT moderni sono eccellenti nel dimostrare l'insoddisfacibilità (usando euristiche per l'istantiazione dei quantificatori). Tuttavia, nel caso di soddisfacibilità, tendono a fallire o a richiedere tempi eccessivi quando:
  1. Il modello minimo non è finito (es. funzioni definite ricorsivamente su interi infiniti).
  2. Il modello finito è troppo grande per essere costruito esplicitamente.
  3. Le formule non appartengono a classi decibili note.
• Esempio critico: Formule semplici come $f(0) = 0 \land \forall x . f(x + 1) = f(x) + 1$ non hanno modelli finiti, rendendo impossibile la costruzione esplicita di un modello da parte dei solver tradizionali.

2. Metodologia

Gli autori propongono un approccio alternativo che non costruisce esplicitamente un modello completo, ma certifica la soddisfacibilità utilizzando argomenti induttivi.

Concetti Chiave:

• Certificati di Soddisfacibilità: Invece di un modello completo, si definisce un "certificato" che rappresenta una prova induttiva. Questo certificato è composto da:
  1. Una pre-soddisfacibilità: un'interpretazione parziale (cella) che soddisfa la parte quantificata libera ($F$) e fornisce valori per gli argomenti delle funzioni non interpretate nella parte quantificata ($Q$).
  2. Un ordine ben fondato ($\preceq$) sul dominio delle variabili quantificate.
  3. Un propagatore di soddisfacibilità: una funzione che, per ogni passo dell'induzione (ogni valore $z$ dell'ordine), dimostra l'esistenza di valori per le "celle propagate" (nuove istanze di funzioni) tali che la formula quantificata rimanga vera.
• Condizione ReqPivot: Per garantire che l'induzione funzioni verso l'infinito (sia in aumento che in diminuzione), la formula deve soddisfare una condizione semantica chiamata ReqPivot. Questa condizione richiede che esistano sottoinsiemi di termini "estremali" per i quali sia possibile propagare i valori al di fuori di un intervallo base senza creare conflitti con la parte quantificata libera.
• Algoritmo Proposto:
  1. L'algoritmo cerca un intervallo intero finito $B = [b_{min}, b_{max}]$.
  2. Verifica la soddisfacibilità della formula istanziata su $B$.
  3. Verifica le condizioni di propagabilità ($\Psi^+$ e $\Psi^-$) che garantiscono che la soluzione possa essere estesa all'infinito verso l'alto e verso il basso senza conflitti.
  4. Se tali condizioni sono soddisfatte, restituisce "Sat" (Soddisfacibile) e genera un certificato.

Implementazione Tecnica:

• Per evitare l'esplosione combinatoria nella verifica delle sottoinsiemi di termini, gli autori introducono una codifica CNF compatta utilizzando variabili booleane ausiliarie per rappresentare la scelta dei termini estremali.
• L'algoritmo è stato implementato utilizzando l'API Python di Z3.

3. Contributi Chiave

1. Nuova Definizione di Certificato: Introduzione di un concetto di certificato di soddisfacibilità basato sull'induzione, che permette di ragionare su modelli infiniti senza costruirli esplicitamente.
2. Algoritmo per UFLIA: Sviluppo di un algoritmo specifico per la logica UFLIA (con restrizioni su coefficienti uniformi e un solo quantificatore) che dimostra la soddisfacibilità per formule fuori dalla portata degli attuali solver.
3. Condizioni di Correttezza: Dimostrazione della correttezza (soundness) e completezza relativa (se la formula soddisfa la condizione ReqPivot) dell'algoritmo.
4. Codifica Efficiente: Proposta di una codifica proposizionale (CNF) che rende la verifica delle condizioni di propagazione computazionalmente fattibile.
5. Generazione di Modelli: Descrizione di come estrarre valori concreti per le funzioni non interpretate dal certificato, permettendo la costruzione di un modello (sebbene potenzialmente infinito) in modo ricorsivo.

4. Risultati Sperimentali

Gli autori hanno testato il loro approccio su un set di 28 problemi costruiti a mano, confrontandolo con solver SMT all'avanguardia (Z3 e CVC5).

• Performance del nuovo algoritmo:
  • Termina in tempo trascurabile su tutti i problemi.
  • È insensibile alla dimensione del modello (parametro $c$ che estende il dominio), grazie all'uso dell'induzione.
• Confronto con Z3 e CVC5:
  • Z3: Fallisce spesso restituendo "Unknown" o timeout man mano che la dimensione del modello richiesto aumenta (es. per $c \ge 2$). Risolve solo 4 problemi su 28 senza limiti di dominio.
  • CVC5 (Modalità standard): Fallisce su molti problemi con $c \ge 3$ (timeout).
  • CVC5 (Modalità SyGuS): Risolve 15 problemi, ma solo se le funzioni rientrano in grammatiche predefinite. Fallisce su formule che richiedono funzioni non esprimibili nella grammatica di default (es. $f(x+1) = 2*f(x)$).
• Conclusione sperimentale: L'approccio basato sull'induzione supera significativamente gli attuali solver SMT nella capacità di dimostrare la soddisfacibilità di formule con modelli infiniti o grandi, senza dipendere da grammatiche sintattiche rigide come SyGuS.

5. Significato e Impatto

• Superamento dei limiti attuali: Il lavoro dimostra che è possibile certificare la soddisfacibilità di formule che non ammettono modelli finiti, un caso in cui i metodi basati sulla costruzione esplicita di modelli falliscono inevitabilmente.
• Applicabilità: La metodologia è particolarmente rilevante per la verifica di programmi, dove le proprietà degli array sono spesso espresse tramite quantificatori universali e funzioni non interpretate.
• Visione Futura: Gli autori mirano a generalizzare l'algoritmo per renderlo parametrico rispetto alle teorie sottostanti (non solo interi lineari) e a rilassare la condizione ReqPivot utilizzando forme di induzione più potenti, puntando verso un algoritmo generale per la soddisfacibilità in logiche miste.

In sintesi, il paper introduce un cambio di paradigma: invece di cercare un modello (che potrebbe non esistere in forma finita), si cerca una prova strutturale (certificato) che garantisca l'esistenza di un modello attraverso l'induzione, offrendo una soluzione robusta a un problema aperto nella logica dei predicati e nell'automated reasoning.