Automated Reencoding Meets Graph Theory

Titel: Automatische Hercodering ontmoet Graphentheorie

Auteurs: Benjamin Przybocki, Bernardo Subercaseaux, Marijn J. H. Heule (Carnegie Mellon University)

---

1. Probleemstelling

Moderne SAT-solvers (oplossers voor Boolese satisfiabiliteit) presteren opmerkelijk goed in de praktijk, maar de theoretische onderbouwing van hun succes is complex. Een cruciaal onderdeel van deze solvers is Bounded Variable Addition (BVA), een voorverwerkingsmethode die extra variabelen introduceert om een formule te herschrijven in een equivalente formule met minder clausules.

Hoewel BVA empirisch zeer succesvol is (bijvoorbeeld in de winnaars van de SAT Competitie 2023 en 2024), ontbreekt er een diepgaand theoretisch inzicht in:

• Welke herschrijvingen (re-encodings) zijn theoretisch mogelijk met BVA?
• Wat zijn de fundamentele beperkingen van BVA?
• Hoe verhoudt BVA zich tot andere optimalisatietechnieken?
• Kan BVA specifieke, efficiënte coderingen (zoals de "product encoding" voor de at-most-one constraint) automatisch genereren?

Het doel van dit artikel is om deze vragen te beantwoorden door BVA te analyseren via een graph-theoretisch raamwerk, met een focus op 2-CNF formules (formules waarbij elke clausule uit precies twee literalen bestaat).

2. Methodologie: Graph-theoretisch Raamwerk

De auteurs ontwikkelen een nieuwe theoretische benadering die BVA koppelt aan het concept van Strict Polarized Rectifier Networks (SPRN).

• Van Formule naar Graph: Een 2-CNF formule wordt gemodelleerd als een "diagram" (een graaf met zowel gerichte als ongerichte randen). Gerichte randen $(u, v)$ corresponderen met implicaties ($u \to v$), terwijl ongerichte randen $\{u, v\}$ corresponderen met clausules $(u \lor v)$.
• BVA als Graph-transformatie: Een BVA-stap, waarbij een biclique (volledig bipartiete subgraaf) wordt vervangen door een nieuwe variabele, wordt geïnterpreteerd als het reduceren van de graaf door een nieuwe knooppunt (hulpvariabele) in te voeren die de connectiviteit behoudt.
• Strict Polarized Rectifier Networks (SPRN): De auteurs definiëren SPRN's als een specifiek type graaf dat de beperkingen van BVA weerspiegelt. Een SPRN mag geen "dangling" hulpvariabelen hebben en mag geen twee basisvariabelen via meerdere geldige wandelingen (valid walks) met elkaar verbinden.
• Hoofdstelling (Theorema 5): Er bestaat een directe correspondentie tussen formules die met BVA kunnen worden herschreven en SPRN's die het oorspronkelijke diagram realiseren. Dit betekent dat BVA precies die herschrijvingen kan uitvoeren die overeenkomen met SPRN's.

3. Belangrijkste Bijdragen en Resultaten

A. Theoretische Grenzen voor Algemene 2-CNF Formules

De auteurs bewijzen scherpe boven- en ondergrenzen voor het aantal clausules na herschrijving:

• Zonder extra voorverwerking: Idealized BVA kan elke 2-CNF formule met $n$ variabelen herschrijven naar een formule met maximaal $(1 + o(1)) \frac{n^2}{\lg n}$ clausules. Dit is een aanzienlijke verbetering ten opzichte van de oorspronkelijke $\Theta(n^2)$ clausules.
• Met voorverwerking (Simplification): Door vooraf equivalentie van literalen te substitueren en "failed literal elimination" toe te passen, verbetert de bovengrens naar:
  $$\left(\frac{\lg(3)}{4} + o(1)\right) \frac{n^2}{\lg n} \approx 0.396 \frac{n^2}{\lg n}$$
• Optimaliteit: Ze bewijzen dat geen enkele herschrijvingsmethode (die outputt in 2-CNF) een constante factor onder de $0.25$ kan bereiken. Idealized BVA is dus optimaal tot op een constante factor.

B. Monotone 2-CNF Formules

Voor monotone formules (alleen positieve literalen) kunnen ze een nog betere bovengrens bewijzen:

• Idealized BVA kan monotone 2-CNF formules herschrijven naar maximaal $(\frac{1}{4} + o(1)) \frac{n^2}{\lg n}$ clausules.
• Dit komt overeen met de theoretische ondergrens voor elke herschrijvingsmethode op monotone formules, wat suggereert dat BVA voor dit specifieke geval bijna optimaal is.

C. De "At-Most-One" (AMO) Constraint

Een van de meest praktische en gestructureerde 2-CNF formules is de at-most-one constraint (maximaal één variabele mag waar zijn).

• Empirische observatie: Bestaande implementaties van BVA reduceren de directe codering ($\binom{n}{2}$ clausules) naar $3n - 6$ clausules.
• Theoretisch bewijs: De auteurs bewijzen dat geen enkele implementatie van BVA (ongeacht de heuristieken) de AMO-constraint kan herschrijven naar minder dan $3n - 6$ clausules.
• Gevolg: Dit betekent dat BVA niet in staat is om de "product encoding" te genereren, die slechts $2n + o(n)$ clausules gebruikt. Dit verklaart waarom BVA bepaalde structurele optimalisaties niet kan bereiken, zelfs niet met slimme heuristieken.

D. Efficiëntere Implementatie (BiVA)

Gebaseerd op recente algoritmen voor het partitioneren van bicliques in grafen (Krapivin et al.), ontwikkelen de auteurs een nieuwe implementatie genaamd BiVA.

• Complexiteit: De oude implementatie (factor in CaDiCaL/Kissat) heeft een complexiteit van ten minste $\Omega(n^3)$. De nieuwe BiVA werkt in $O(n^2)$.
• Prestaties: Op willekeurige monotone 2-CNF formules levert BiVA een snelheidswinst van een orde van grootte op, terwijl het een vergelijkbare clausule-reductie bereikt als de bestaande methoden.

4. Experimentele Validatie

De auteurs testen hun theorie op formules die het Independent Set-probleem modelleren op willekeurige grafen $G(n, 1/2)$.

• Vergelijking: Ze vergelijken BiVA, de standaard BVA, factor, en combinaties (BiVA + BVA).
• Resultaten:
  • De clausule-reductie is vergelijkbaar tussen alle methoden (BiVA is soms iets minder effectief, maar dit wordt gecompenseerd door snellere uitvoering).
  • De combinatie van BiVA gevolgd door BVA of factor is aanzienlijk sneller dan het gebruik van BVA of factor alleen, omdat de tweede stap op een reeds gecomprimeerde formule werkt.
  • BiVA introduceert minder hulpvariabelen dan de andere methoden, wat gunstig is voor de geheugenefficiëntie.

5. Betekenis en Conclusie

Dit artikel levert een fundamentele bijdrage aan het theoretisch begrip van SAT-preprocessing:

1. Theoretische Limieten: Het definieert precies wat BVA kan en niet kan doen, en toont aan dat er een fundamentele kloof bestaat tussen wat BVA kan bereiken en de theoretisch optimale coderingen voor bepaalde structuren (zoals AMO).
2. Graph Theory Koppeling: Het koppelt succesvol SAT-preprocessing aan geavanceerde concepten uit de graphentheorie (rectifier networks), wat nieuwe inzichten biedt voor zowel theoretici als practitioners.
3. Praktische Impact: De ontwikkeling van BiVA demonstreert dat theoretische inzichten direct kunnen leiden tot significante praktische snelheidswinsten (van $\Omega(n^3)$ naar $O(n^2)$).

Samenvattend toont het paper aan dat hoewel BVA een krachtige techniek is, het geen "wondermiddel" is voor alle structuren. De beperkingen van BVA zijn inherent aan de manier waarop het implicaties construeert (via SPRN's), en het doorbreken van deze grenzen vereist waarschijnlijk nieuwe, niet-BVA-gebaseerde herschrijvingsmethoden.