Riepilogo Tecnico: Oltre le Codifiche Eager: Un Approccio Agnostico alla Teoria per l'Enumerazione di Lemma Teorici in SMT

1. Enunciato del Problema

Nella Soddisfacibilità Modulo Teorie (SMT), l'innalzamento delle tecniche di ragionamento booleano richiede spesso la generazione di lemma teorici (T-lemma). Si tratta di clausole T-validhe che escludono assegnazioni di verità che sono proposizionalmente soddisfacenti ma T-inconsistenti.

Mentre la risoluzione SMT standard genera questi lemma "lazy" su richiesta durante la ricerca, certi compiti SMT complessi—come l'estrazione del minimo unsat-core, MaxSMT e la compilazione di T-OBDD o T-SDD—richiedono il pre-calcolo "eager" di un insieme completo di T-lemma in anticipo.

Le codifiche "classiche" eager SMT esistenti sono insufficienti a questo scopo perché:

1. Sono specifiche per poche teorie semplici (ad es. EUF, DL, LRA).
2. Non rispettano la combinazione delle teorie.
3. Spesso producono un numero eccessivo di lemma non necessari.

Attualmente, manca un metodo agnostico alla teoria per enumerare efficientemente insiemi completi di T-lemma per formule arbitrarie, in particolare per le applicazioni di Compilazione della Conoscenza (KC) dove il sovraccarico computazionale viene spostato in una fase offline per abilitare query online a tempo polinomiale.

2. Metodologia

Gli autori propongono un framework per l'enumerazione di T-lemma che è agnostico rispetto alla teoria sottostante. L'approccio si basa su un metodo di base che utilizza AllSMT (enumerazione di tutte le assegnazioni T-soddisfacenti) e introduce tre miglioramenti ortogonali e componibili per migliorare la scalabilità:

2.1 Base: Enumerazione Totale AllSMT

Il metodo di base (Algoritmo 2) esegue un'enumerazione AllSMT totale, non proiettata, sulla formula di input $\phi[\alpha]$. Iterativamente trova assegnazioni di verità totali T-soddisfacenti, le blocca e raccoglie i T-lemma appresi dal solver fino a quando la formula diventa insoddisfacibile.

• Limitazione: Questo approccio si basa sull'enumerazione di assegnazioni totali. Come dimostrato nell'Esempio 2, una enumerazione parziale ingenua può fallire nel generare i T-lemma necessari perché il solver potrebbe non esplorare mai l'assegnazione totale T-incoerente specifica che innesca un conflitto. Tuttavia, l'enumerazione di tutte le assegnazioni totali è spesso computazionalmente intrattabile a causa dell'esplosione combinatoria.

2.2 Miglioramento 1: Divide-and-Conquer (D&C)

Per mitigare il costo dell'enumerazione totale, gli autori propongono una strategia Divide-and-Conquer (Algoritmo 3):

1. Eseguire un'enumerazione parziale AllSMT per decomporre lo spazio di ricerca booleano in un insieme di assegnazioni parziali disgiunte e T-soddisfacenti ($M_{\alpha}^p$).
2. Per ogni assegnazione parziale $\mu \in M_{\alpha}^p$, eseguire un'enumerazione totale AllSMT sulla formula ristretta $\phi \land \mu$.
3. Le enumerazioni totali vengono eseguite in parallelo.

• Razionale: Questo trasforma un'unica grande enumerazione totale intrattabile in un passo di decomposizione più economico più molte enumerazioni totali più piccole e gestibili.

2.3 Miglioramento 2: Enumerazione Proiettata

Gli autori osservano che l'incoerenza T è determinata esclusivamente dall'assegnazione agli atomi della teoria ($\alpha_T$), non agli atomi booleani ($\alpha_B$).

• Metodo: Eseguire un'enumerazione AllSMT proiettata solo su $\alpha_T$ (Algoritmo 4).
• Base Teorica: Il Teorema 1 dimostra che proiettare l'enumerazione sugli atomi T produce un insieme completo di T-lemma.
• Vantaggio: Questo riduce drasticamente la dimensione della ricerca. Una singola assegnazione T-soddisfacente su $\alpha_T$ rappresenta fino a $2^k$ assegnazioni totali sull'insieme completo di atomi (dove $k$ è il numero di atomi booleani), riducendo significativamente l'uso di memoria e la dimensione delle clausole di blocco.

2.4 Miglioramento 3: Partizionamento Guidato dalla Teoria

Se l'insieme degli atomi in $\phi$ può essere partizionato in insiemi disgiunti ($\alpha_1, \dots, \alpha_n$) tali che nessun atomo in un insieme condivide variabili o simboli non interpretati con gli atomi in un altro, il problema può essere ulteriormente decomposto (Algoritmo 5).

• Metodo: Basato sulla Proprietà 1 e sul Teorema 2, i T-lemma possono essere enumerati indipendentemente per ogni partizione. L'algoritmo partiziona iterativamente gli atomi, enumera i lemma per ogni partizione proiettata sugli atomi di quella partizione e accumula i risultati.
• Vantaggio: Questo permette la decomposizione di un'unica enumerazione totale in $n$ enumerazioni proiettate indipendenti, offrendo potenziali accelerazioni esponenziali per problemi con componenti disgiunte.

3. Contributi Chiave

1. Framework Agnostico alla Teoria: La prima presentazione esplicita di metodi per enumerare insiemi completi di T-lemma per teorie arbitrarie, andando oltre le codifiche eager specifiche per teoria.
2. Tecniche di Scalabilità: L'introduzione di tre tecniche ortogonali:
   • Divide-and-Conquer: Parallelizza la ricerca decomponendo lo spazio booleano.
   • Enumerazione Proiettata: Riduce la dimensionalità della ricerca concentrandosi sugli atomi T.
   • Partizionamento: Sfrutta la disgiunzione strutturale nella formula per risolvere i sottoproblemi indipendentemente.
3. Garanzie Teoriche: Prove formali (Teoremi 1 e 2) che dimostrano che queste ottimizzazioni preservano la completezza dell'insieme di T-lemma necessario per escludere tutte le assegnazioni T-incoerenti.
4. Integrazione con la Compilazione della Conoscenza: Il lavoro funge da tecnica abilitante per l'innalzamento dei metodi di Compilazione della Conoscenza (in particolare i Diagrammi di Decisione come OBDD e SDD) al livello SMT, affrontando il precedente collo di bottiglia dell'enumerazione dei T-lemma.

4. Risultati Sperimentali

Le tecniche sono state valutate su due insiemi di benchmark:

• Istanze Sintetiche SMT(LRA): 450 problemi generati casualmente da [16].
• Istanze di Pianificazione Temporale: 90 codifiche SMT di problemi di pianificazione nel dominio "Painter".

Metriche di Prestazione:

• Efficienza Temporale:
  • Sui benchmark sintetici, D&C ha migliorato le prestazioni fino a 2 ordini di grandezza rispetto alla base, risolvendo 17 problemi in più entro il timeout.
  • L'aggiunta della Proiezione ha ulteriormente migliorato i risultati, risolvendo 30 problemi in più rispetto al solo D&C e riducendo drasticamente il tempo per le istanze precedentemente risolte.
  • Il Partizionamento non ha mostrato miglioramenti sui dati sintetici (poiché pochi problemi avevano partizioni disgiunte) ma è stato altamente efficace sui problemi di pianificazione.
  • Sui problemi di pianificazione, il Partizionamento è stato il fattore dominante, permettendo la risoluzione di problemi con orizzonte 5 che erano precedentemente intrattabili, raggiungendo accelerazioni di diversi ordini di grandezza.
• Numero di Lemma:
  • D&C tendeva a produrre leggermente più lemma a causa della ridondanza parallela.
  • Proiezione e Partizionamento hanno generalmente ridotto il numero di lemma enumerati mitigando l'esplorazione ridondante e generando lemma più forti e più piccoli.
• Dimensione dei Lemma:
  • Il partizionamento sui problemi di pianificazione ha portato a T-lemma significativamente più piccoli (meno letterali), probabilmente a causa della potatura precoce dei rami T-incoerenti che coinvolgono solo partizioni specifiche.

5. Significato e Affermazioni

Il documento afferma che queste tecniche migliorano drasticamente l'efficienza e la scalabilità dell'enumerazione dei T-lemma rispetto all'approccio AllSMT di base.

• Ruolo Abilitante: Il significato principale è l'abilitazione dell'applicazione pratica della Compilazione della Conoscenza all'SMT. Gli autori notano che nel loro lavoro precedente [16], l'enumerazione dei T-lemma era il "principale collo di bottiglia" per la compilazione dei Diagrammi di Decisione. Risolvendo questo collo di bottiglia, i metodi proposti aprono la strada alla scalabilità di queste tecniche di compilazione su istanze complesse e reali.
• Modestia: Gli autori sono attenti a notare che i miglioramenti dipendono dal contesto. Ad esempio, la proiezione non ha aiutato con i problemi di pianificazione perché le assegnazioni degli atomi T erano conseguenze deterministiche delle assegnazioni booleane in quelle specifiche codifiche. Analogamente, il partizionamento ha prodotto benefici solo quando la struttura del problema permetteva naturalmente partizioni disgiunte.

In sintesi, il documento fornisce un toolkit robusto e agnostico alla teoria per l'enumerazione eager dei T-lemma, trasformando un passo precedentemente intrattabile in un processo scalabile, facilitando così applicazioni SMT avanzate come MaxSMT e Compilazione della Conoscenza.