Riepilogo Tecnico: Apprendimento di Clausole con Risoluzione Estesa tramite Punti di Doppia Implicazione

Enunciato del Problema

I solutori SAT basati sull'apprendimento di clausole guidato dai conflitti (CDCL) sono diventati onnipresenti nell'ingegneria del software, nella sicurezza e nell'intelligenza artificiale. Tuttavia, nonostante il loro successo pratico, sono fondamentalmente limitati dalla loro dipendenza dal sistema di prova della risoluzione generale (Res), noto per essere debole su certe classi di formule (ad esempio, il Principio della Cassa dei Piccioni, le formule di Tseitin). Sebbene esistano sistemi di prova più potenti come la Risoluzione Estesa (ER) e possano fornire prove di dimensione polinomiale per questi casi difficili, l'integrazione dell'ER nei solutori CDCL rimane una sfida significativa. I metodi esistenti, come GlucosER, introducono variabili estese dinamicamente ma si affidano a schemi specifici di lemma appresi (lemma consecutivi che condividono un suffisso comune) per identificare nuove variabili. Gli autori identificano la necessità di un approccio più flessibile e generale per l'introduzione dinamica di variabili estese all'interno del ciclo di analisi dei conflitti del CDCL, al fine di migliorare le prestazioni del solutore su problemi combinatori difficili.

Metodologia

Il documento propone un nuovo algoritmo per l'Apprendimento di Clausole con Risoluzione Estesa (ERCL) implementato all'interno del solutore CDCL MapleLCM, dando vita a un nuovo sistema denominato xMapleLCM. L'innovazione centrale è l'uso dei Punti di Doppia Implicazione (DIP) per introdurre dinamicamente nuove variabili.

1. Punti di Doppia Implicazione (DIP)

Un DIP è definito come una generalizzazione del Punto di Implicazione Unica (UIP). Mentre un UIP è un singolo letterale che domina tutti i percorsi dal livello di decisione più alto al nodo di conflitto nel grafo di implicazione, un DIP è una coppia di letterali $\{x, y\}$ tale che:

• Ogni percorso dalla variabile di decisione al livello di decisione più alto fino al nodo di conflitto passa attraverso almeno un nodo della coppia.
• Né $x$ né $y$ sono un UIP.

Gli autori riformulano il problema della ricerca dei DIP come la ricerca di Dominatori di Due Vertici (TVD) in un grafo diretto. Utilizzano un algoritmo a tempo lineare (dettagliato in un documento complementare [BGO24]) basato sul teorema di Menger e sull'identificazione di percorsi disgiunti per vertice per trovare efficientemente tutte le coppie DIP valide.

2. Algoritmo ERCL e Introduzione di Variabili

Quando un DIP $\{a, b\}$ viene identificato durante l'analisi dei conflitti, il solutore introduce una nuova variabile di estensione $z$ definita come $z \leftrightarrow a \land b$. Ciò permette al solutore di apprendere due nuovi tipi di clausole:

• Clausola Pre-DIP: Derivata dall'implicazione che il primo UIP e certi letterali dai livelli di decisione precedenti implicano la coppia DIP. Formalmente: $\neg f \lor \neg C \lor z$ (dove $f$ è il primo UIP e $C$ rappresenta i letterali che portano al DIP).
• Clausola Post-DIP: Derivata dall'implicazione che la coppia DIP e certi letterali portano a un conflitto. Formalmente: $\neg z \lor \neg D$.

Questo processo riduce efficacemente la lunghezza delle clausole apprese sostituendo congiunzioni complesse con una singola variabile, potenzialmente riducendo lo spazio di ricerca.

3. Implementazione ed Euristiche

Gli autori hanno implementato xMapleLCM come un framework altamente estensibile. Le decisioni euristica chiave includono:

• Selezione del DIP: Le strategie includono la scelta del DIP più vicino al conflitto, del DIP "centrale" (bilanciando il grafo) o la selezione casuale.
• Filtraggio: Meccanismi per scartare DIP di bassa qualità, come richiedere un conteggio minimo di occorrenze (ad esempio, 20 o 50 volte) o verificare se la risultante clausola post-DIP è una clausola "collante" (LBD = 2).
• Apprendimento di Clausole: Opzioni per apprendere sia le clausole pre- che post-DIP o solo la clausola post-DIP.
• Gestione delle Variabili: Una strategia per eliminare le variabili estese che non sono più attive (ad esempio, eliminando il 50% peggiore delle variabili ogni 1000 conflitti) per prevenire il rallentamento del solutore.
• Commutazione Adattiva: Un'euristica che monitora la percentuale di decisioni prese sulle variabili estese. Se questa percentuale scende sotto una soglia (3%), il solutore torna all'apprendimento standard 1-UIP per evitare sovraccarichi su istanze in cui l'ER non è vantaggioso.

Contributi Chiave

1. Concetto di DIP: L'introduzione dei Punti di Doppia Implicazione come generalizzazione degli UIP, fornendo un nuovo strumento strutturale per l'analisi dei grafi dei conflitti.
2. Algoritmo a Tempo Lineare: Un algoritmo efficiente per calcolare tutti i DIP nel grafo di implicazione, rendendo l'approccio fattibile per l'uso a runtime nei solutori SAT.
3. Framework ERCL Flessibile: Lo sviluppo di xMapleLCM, un sistema parametrizzabile che permette agli sviluppatori di sperimentare varie politiche di selezione dei DIP, filtraggio e apprendimento di clausole.
4. Validazione Empirica: Una valutazione estesa che dimostra come l'ERCL basato su DIP superi significativamente i solutori CDCL standard e altri solutori su specifici benchmark combinatori difficili.

Risultati Sperimentali

Gli autori hanno valutato xMapleLCM contro solutori leader (Kissat, CryptoMiniSat, SBVA-CaDiCaL, GlucosER) su quattro famiglie distinte di benchmark:

• Formule di Tseitin: Sulle formule di Tseitin basate su griglia, xMapleLCM è stato l'unico solutore a risolvere tutte le istanze entro il limite di tempo di 600 secondi. Mentre GlucosER ha funzionato bene sulle formule di Tseitin regolari, ha faticato con le istanze basate su griglia. I solutori CDCL standard (Kissat, SBVA-CaDiCaL) hanno avuto prestazioni scarse.
• Formule k-XOR Casuali Xorificate: xMapleLCM e GlucosER hanno superato significativamente gli altri solutori. CryptoMiniSat, che utilizza l'eliminazione di Gauss, ha avuto successo solo su istanze più piccole o impostazioni specifiche di xorificazione, fallendo nel scalare su formule più grandi e difficili.
• Problemi di Corrispondenza di Intervalli: Per queste istanze insoddisfacibili, nessun solutore senza ragionamento sulla risoluzione estesa è riuscito a risolvere alcun benchmark entro un limite di 2 ore. xMapleLCM e GlucosER hanno risolto tutte le istanze, con xMapleLCM leggermente più lento ma comparabile.
• SAT Competition 2023 Main Track: Su benchmark generali, xMapleLCM ha performance simili al suo solutore base (MapleLCM). Il meccanismo di commutazione adattiva ha prevenuto con successo il degrado delle prestazioni su istanze in cui l'ER non era utile, mantenendo allo stesso tempo la capacità di risolvere istanze specifiche difficili per l'ER.

Gli autori notano che circa il 63% dei conflitti nei loro esperimenti conteneva almeno un DIP, giustificando la necessità di meccanismi di filtraggio. Hanno anche osservato che xMapleLCM e GlucosER identificano insiemi diversi di variabili estese (solo ~25% di sovrapposizione), suggerendo che catturano proprietà semantiche diverse.

Significato e Affermazioni

Il documento afferma che la risoluzione estesa può essere integrata con successo nei solutori CDCL per risolvere classi di formule che altrimenti sarebbero intrattabili per i solutori basati sulla risoluzione standard.

• Complementarità: Il lavoro dimostra che esistono modi multipli validi per automatizzare l'ER (approccio basato su DIP rispetto all'approccio basato su lemma di GlucosER), e entrambi possono essere efficaci sulle stesse classi di problemi difficili.
• Praticità: Gli autori mostrano che l'overhead del rilevamento dei DIP è trascurabile (tipicamente <2,5% del tempo di esecuzione) e che il metodo non degrada le prestazioni sui benchmark generali quando vengono utilizzate euristiche adattive.
• Direzione Futura: Il documento posiziona i DIP come fondamento per ulteriori ricerche, inclusa l'esplorazione di Punti di k-Implicazione ($k > 2$) e l'applicazione di euristiche di apprendimento automatico per ottimizzare meglio le strategie ERCL.

Gli autori concludono modestamente che, sebbene abbiano identificato famiglie specifiche in cui l'ERCL è superiore, la questione teorica se l'ER basato su DIP simuli completamente l'ER illimitato rimane aperta ed è un obiettivo per future indagini teoriche.