Technische Samenvatting: Voorbij Eager Encodings: Een Theorie-onafhankelijke Aanpak voor Theorie-Lemma-Enumeratie in SMT

1. Probleemstelling

In Satisfiability Modulo Theories (SMT) vereist het tillen van Boolese redeneertechnieken vaak het genereren van theorielemma's (T-lemma's). Dit zijn T-geldige clausules die waarheidstoewijzingen uitsluiten die propositorisch bevredigend zijn maar T-inconsistent.

Hoewel standaard SMT-oplossing deze lemma's "lazy" op vraag genereert tijdens het zoeken, vereisen bepaalde complexe SMT-taken—zoals het extraheren van een minimaal onbevredigbaar kern, MaxSMT, en het compileren van T-OBDD's of T-SDD's—de "eager" voorafgaande berekening van een volledige set T-lemma's.

Bestaande "klassieke" eager SMT-encodings zijn onvoldoende voor dit doel omdat:

1. Ze specifiek zijn voor een paar eenvoudige theorieën (bijv. EUF, DL, LRA).
2. Ze niet voldoen aan theoriecombinatie.
3. Ze vaak een overmatig aantal onnodige lemma's produceren.

Momenteel ontbreekt het aan theorie-onafhankelijke methoden om complete sets van T-lemma's efficiënt te enumereren voor willekeurige formules, met name voor Knowledge Compilation (KC)-toepassingen waarbij rekenkundige overhead wordt verschoven naar een offline-fase om polynomiale online-query's mogelijk te maken.

2. Methodologie

De auteurs stellen een raamwerk voor voor het enumereren van T-lemma's dat onafhankelijk is van de onderliggende theorie. De aanpak bouwt voort op een basismethode met AllSMT (enumereren van alle T-bevredigbare toewijzingen) en introduceert drie orthogonale, combineerbare verbeteringen om de schaalbaarheid te vergroten:

2.1 Baseline: Totale AllSMT-Enumeratie

De basismethode (Algoritme 2) voert een totale, niet-geprojecteerde AllSMT-Enumeratie uit op de inputformule $\phi[\alpha]$. Het vindt iteratief T-bevredigbare totale waarheidstoewijzingen, blokkeert deze en verzamelt T-lemma's die door de solver zijn geleerd totdat de formule onbevredigbaar wordt.

• Beperking: Deze aanpak is afhankelijk van het enumereren van totale toewijzingen. Zoals aangetoond in Voorbeeld 2, kan naïeve partiële enumeratie falen om noodzakelijke T-lemma's te genereren omdat de solver mogelijk nooit de specifieke T-inconsistente totale toewijzing onderzoekt die een conflict veroorzaakt. Het enumereren van alle totale toewijzingen is echter vaak computationeel onuitvoerbaar vanwege combinatorische explosie.

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

Om de kosten van totale enumeratie te beperken, stellen de auteurs een Divide-and-Conquer-strategie voor (Algoritme 3):

1. Voer een partiële AllSMT-Enumeratie uit om de Boolese zoekruimte te decomponeren in een set disjuncte, T-bevredigbare partiële toewijzingen ($M_{\alpha}^p$).
2. Voor elke partiële toewijzing $\mu \in M_{\alpha}^p$, voer een totale AllSMT-Enumeratie uit op de beperkte formule $\phi \land \mu$.
3. De totale enumeraties worden parallel uitgevoerd.

• Redenering: Dit transformeert één grote, onuitvoerbare totale enumeratie in één goedkopere decompositiestap plus vele kleinere, hanteerbare totale enumeraties.

2.3 Verbetering 2: Geprojecteerde Enumeratie

De auteurs merken op dat T-inconsistentie uitsluitend wordt bepaald door de toewijzing aan theorie-atomen ($\alpha_T$), niet aan Boolese atomen ($\alpha_B$).

• Methode: Voer AllSMT-Enumeratie uit die alleen is geprojecteerd op $\alpha_T$ (Algoritme 4).
• Theoretische Basis: Stelling 1 bewijst dat het projecteren van de enumeratie op T-atomen een complete set T-lemma's oplevert.
• Voordeel: Dit vermindert de zoekdimensionaliteit drastisch. Eén T-bevredigbare toewijzing op $\alpha_T$ vertegenwoordigt tot $2^k$ totale toewijzingen op de volledige set atomen (waarbij $k$ het aantal Boolese atomen is), wat het geheugengebruik en de grootte van blokkerende clausules aanzienlijk vermindert.

2.4 Verbetering 3: Theorie-gedreven Partitionering

Als de set atomen in $\phi$ kan worden gepartitioneerd in disjuncte sets ($\alpha_1, \dots, \alpha_n$) zodanig dat geen atoom in één set variabelen of ongeïnterpreteerde symbolen deelt met atomen in een andere set, kan het probleem verder worden gecomprimeerd (Algoritme 5).

• Methode: Gebaseerd op Eigenschap 1 en Stelling 2 kunnen T-lemma's onafhankelijk voor elke partition worden genummerd. Het algoritme partitioneert atomen iteratief, enumerert lemma's voor elke partition geprojecteerd op de atomen van die partition, en cumuleert de resultaten.
• Voordeel: Dit maakt het decomponeren van één totale enumeratie in $n$ onafhankelijke geprojecteerde enumeraties mogelijk, wat potentiële exponentiële snelheidswinst biedt voor problemen met disjuncte componenten.

3. Belangrijkste Bijdragen

1. Theorie-onafhankelijk Raamwerk: De eerste expliciete presentatie van methoden om complete sets van T-lemma's te enumereren voor willekeurige theorieën, verdergaand dan theorie-specifieke eager encodings.
2. Schaalbaarheidstechnieken: De introductie van drie orthogonale technieken:
   • Divide-and-Conquer: Paralleliseert het zoeken door de Boolese ruimte te decomponeren.
   • Geprojecteerde Enumeratie: Vermindert de zoekdimensionaliteit door te focussen op T-atomen.
   • Partitionering: Benut structurele disjunctie in de formule om subproblemen onafhankelijk op te lossen.
3. Theoretische Waarborgen: Formele bewijzen (Stellingen 1 en 2) die aantonen dat deze optimalisaties de volledigheid van de set T-lemma's behouden die nodig is om alle T-inconsistente toewijzingen uit te sluiten.
4. Integratie met Knowledge Compilation: Het werk dient als een faciliterende techniek voor het tillen van Knowledge Compilation-methoden (specifiek Beslissingsdiagrammen zoals OBDD's en SDD's) naar het SMT-niveau, waarbij de eerdere bottleneck van T-lemma-Enumeratie wordt aangepakt.

4. Experimentele Resultaten

De technieken werden geëvalueerd op twee benchmarksets:

• Synthetische SMT(LRA)-instanties: 450 willekeurig gegenereerde problemen uit [16].
• Temporele Planningsinstanties: 90 SMT-encodings van planningsproblemen uit het domein "Painter".

Prestatiemetingen:

• Tijds-efficiëntie:
  • Op synthetische benchmarks verbeterde D&C de prestaties met tot 2 ordes van grootte ten opzichte van de baseline, en loste 17 problemen meer op binnen de time-out.
  • Het toevoegen van Projectie verbeterde de resultaten verder, waarbij 30 problemen meer werden opgelost dan met D&C alleen, en de tijd voor eerder opgeloste instanties drastisch werd verkort.
  • Partitionering toonde geen verbetering op synthetische data (aangezien weinig problemen disjuncte partitionen hadden), maar was zeer effectief op planningsproblemen.
  • Op planningsproblemen was Partitionering de dominante factor, waardoor problemen met horizon 5 konden worden opgelost die eerder onuitvoerbaar waren, met snelheidswinsten van meerdere ordes van grootte.
• Aantal Lemma's:
  • D&C neigde tot het produceren van iets meer lemma's als gevolg van parallelle redundantie.
  • Projectie en Partitionering verlaagden over het algemeen het aantal genummerde lemma's door redundant onderzoek te beperken en sterkere, kleinere lemma's te genereren.
• Grootte van Lemma's:
  • Partitionering op planningsproblemen resulteerde in aanzienlijk kleinere (minder literalen bevattende) T-lemma's, waarschijnlijk door vroege pruning van T-inconsistente takken die alleen specifieke partitionen betroffen.

5. Betekenis en Claims

Het artikel stelt dat deze technieken de efficiëntie en schaalbaarheid van T-lemma-Enumeratie ten opzichte van de baseline AllSMT-aanpak drastisch verbeteren.

• Faciliterende Rol: De belangrijkste betekenis is het mogelijk maken van de praktische toepassing van Knowledge Compilation op SMT. De auteurs merken op dat in hun eerdere werk [16] T-lemma-Enumeratie de "hoofdbottleneck" was voor het compileren van Beslissingsdiagrammen. Door deze bottleneck op te lossen, banen de voorgestelde methoden de weg voor het schalen van deze compilatietechnieken naar complexe, real-world instanties.
• Bescheidenheid: De auteurs zijn voorzichtig om op te merken dat verbeteringen contextafhankelijk zijn. Zo hielp projectie niet bij planningsproblemen omdat de T-atom-toewijzingen in die specifieke encodings deterministische gevolgen waren van Boolese toewijzingen. Evenzo leverde partitionering alleen voordelen op wanneer de probleemstructuur natuurlijk toeliet tot disjuncte partitionen.

Kortom, het artikel biedt een robuust, theorie-onafhankelijk toolkit voor eager T-lemma-Enumeratie, waardoor een eerder onuitvoerbare stap wordt omgezet in een schaalbaar proces, waardoor geavanceerde SMT-toepassingen zoals MaxSMT en Knowledge Compilation worden vergemakkelijkt.