Planted-solution SAT and Ising benchmarks from integer factorization

Probleemstelling

Het benchmarken van satisfiability (SAT) en optimalisatie-oplossers vereist probleeminstanties die drie eigenschappen tegelijk vertonen: realistische structuur, systematische schaalbaarheid en een verifieerbare "ground truth" (de bekende oplossing). Bestaande methoden hebben hierin tekortkomingen:

• Willekeurige ensemble's (zoals uniform random k-SAT) zijn schaalbaar en moeilijk bij de drempelwaarde, maar missen een ingebouwde oplossing om de output van de solver te valideren.
• Handgemaakte instanties uit competitiebibliotheken hebben structuur, maar bieden vaak geen gecontroleerde, single-parameter schaalbaarheid van de moeilijkheidsgraad.
• Bestaande "planted-solution" (ingebouwde oplossing) constructies zijn vaak gebaseerd op willekeurige disordere of algebraïsche planting, en missen de deterministische, lange-afstands-correlaties die kenmerkend zijn voor veel reële computationele problemen.

Het doel van dit werk is het introduceren van een nieuwe klasse van benchmark-instanties die deze gaten opvult door gebruik te maken van de deterministische structuur van gehele getallen factorisatie.

Methodologie

De auteurs presenteren een pipeline die de rekenkundige beperkingen van het vermenigvuldigen van twee priemgetallen $p$ en $q$ (waarbij $N = p \times q$) vertaalt naar een constraint satisfaction probleem.

1. Constructie van de CNF-formule:

   • Gegeven twee priemgetallen $p$ en $q$ met bitlengte $d$, wordt het product $N$ berekend.
   • De binaire vermenigvuldiging wordt gemodelleerd als een schakelkring. Elke kolom in de vermenigvuldigingstabel bevat partiële producten ($p_i \land q_j$).
   • Wanneer een kolom meer dan één entiteit bevat, worden deze samengevoegd (gecontracteerd) met half-adders. Dit genereert sommen (XOR) en carries (AND).
   • De carries propageren naar de volgende kolommen, wat leidt tot een cascade-effect.
   • De bits van het bekende product $N$ worden gebruikt om de uitkomsten van de kolommen te "pinnen" (vastzetten op True of False).
   • Het resultaat is een Conjunctive Normal Form (CNF) formule waarbij de bevredigende toewijzingen overeenkomen met geldige factorisaties van $N$.

2. Booleaanse Preprocessing:

   • Voordat de formule naar DIMACS CNF wordt geconverteerd, ondergaat het systeem een iteratieve logische vereenvoudiging.
   • Dit omvat het verspreiden van gepinde waarden, het vereenvoudigen van AND/XOR-clausules (bijv. $0 \land x = 0$), en het samenvoegen van equivalente variabelen.
   • Dit reduceert het aantal variabelen en clausules aanzienlijk, vooral bij kleinere $d$, maar behoudt de fundamentele structuur.

3. Ising-Compilatie:

   • Voor klassieke en kwantume optimalisatie wordt het residu-systeem omgezet in een kwadratische Ising-Hamiltoniaan.
   • Booleaanse variabelen worden gemapt naar spins ($s_i \in \{-1, +1\}$).
   • Logische constraints (AND en XOR) worden vertaald naar "energy gadgets" (straftermen) die nul zijn voor geldige oplossingen en positief voor onjuiste.
   • XOR-constraints vereisen een extra hulp-spin om kwadratisch te blijven.

Belangrijkste Bijdragen en Theoretische Resultaten

• Schaalbaarheid ($\Theta(d^4)$):
  De auteurs leiden exacte gesloten-vorm uitdrukkingen af voor de grootte van de instanties. Ze bewijzen dat het totale aantal contracties (en dus het aantal variabelen en clausules) schaalt als $O(d^4)$.

  • Oorzaak: Het cascade-effect van de carries. Elke contractie genereert een carry die naar de volgende kolom gaat, wat daar extra contracties vereist. Dit creëert een positieve feedback-lus. De populatie van entiteiten in een kolom groeit kwadratisch met de kolomindex, en het sommeren over $\sim d^2$ actieve kolommen resulteert in een quartische totale groei.
  • Dit onderscheidt de instanties fundamenteel van willekeurige SAT-problemen.

• Lange-afstands-correlaties:
  Door de carry-propagatie zijn variabelen die ver uit elkaar liggen in de vermenigvuldigingstabel (tot op afstand $O(d^2)$) met elkaar verbonden. Dit creëert een complexe, niet-lokale interactiestructuur die moeilijk te ontwarren is voor standaard heuristieken.

• Verifieerbare Ground Truth:
  Omdat de constructie begint met de bekende priemgetallen $(p, q)$, is de oplossing per definitie bekend. Dit maakt het mogelijk om de output van elke solver exact te verifiëren, wat essentieel is voor betrouwbare benchmarks.

• Dual Representatie:
  Dezelfde probleeminstantie kan direct worden gebruikt voor SAT-oplossers (via DIMACS CNF) én voor Ising-optimalisatoren (klassiek of kwantum), wat cross-platform vergelijkingen mogelijk maakt.

Empirische Resultaten

De auteurs hebben de benchmark getest met twee state-of-the-art SAT-oplossers (Kissat 3.0 en CaDiCaL 1.5) voor priemgetallen met bitlengtes $d$ van 8 tot 27.

• Exponentiële Groei: De mediane runtime van de oplossers groeit exponentieel met de bitlengte $d$.
  • De relatie wordt beschreven als $T_{median} \sim 2^{\beta d}$, waarbij $\beta \approx 1$.
  • Dit betekent dat elke extra bit de runtime ongeveer verdubbelt.
• Structuur-gedreven Moeilijkheid: De twee oplossers vertonen bijna identieke schalingsgedragingen, wat suggereert dat de moeilijkheid wordt bepaald door de inherente structuur van de vermenigvuldigingskring (de lange-afstands-correlaties) en niet door solver-specifieke heuristieken.
• Praktische Implicatie: Bij $d=27$ (waarbij $N \approx 10^{16}$) bereiken de runtimes al $\sim 10^4$ seconden. Dit suggereert dat instanties met $d \geq 35-40$ een zware test zullen vormen voor moderne CDCL-solvers.

Betekenis en Toekomstperspectief

Deze benchmark-familie vult een cruciale lacune in het onderzoeksveld:

1. Controleerbaarheid: Het biedt een manier om de prestaties van oplossers te testen op gestructureerde, niet-willekeurige problemen met een bekende oplossing.
2. Kwantum- en Klassieke Optimalisatie: De Ising-vertaling maakt het een ideale testbed voor quantum annealers en klassieke optimalisatie-algoritmen, waarbij de "ground state" exact bekend is.
3. Inzicht in Solver-gedrag: De resultaten tonen aan dat zelfs voor problemen die deterministisch zijn opgebouwd (zoals vermenigvuldiging), de carry-cascades leiden tot een complexiteit die voor huidige oplossers exponentieel schaalt.

De auteurs hebben de volledige generatie-software open-source beschikbaar gesteld, waardoor onderzoekers eenvoudig instanties kunnen genereren voor verschillende waarden van $d$ om de schaalbaarheid van nieuwe algoritmen te testen. Dit werk legt de basis voor een nieuwe standaard in het benchmarken van constraint satisfaction en optimalisatieproblemen.