🔢 mathematics

Queen Domination by SAT Solving

Dit artikel presenteert een hoogwaardig, bewijsgenererend SAT-framework dat het voorheen openstaande $n=19$ koningin-dominantiegeval oplost en de enumeratie voor $n=16$ corrigeert door gebruik te maken van een geometrisch geïnformeerde codering, symmetrie-doorbreking en een verenigde verificatiepijplijn om onafhankelijk verifieerbare correctheid te waarborgen.

Oorspronkelijke auteurs: Taha Rostami, Curtis Bright

Gepubliceerd 2026-07-30

📖 4 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Taha Rostami, Curtis Bright

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je een wereld voor waarin wiskunde niet alleen gaat over getallen op een pagina, maar over het oplossen van puzzels die zo complex zijn dat zelfs de slimste menselijke breinen er duizelig van worden. Dit is het domein van de combinatorische zoektocht, een tak van de informatica en wiskunde die zich bezighoudt met het vinden van de beste manier om dingen te ordenen. Denk hierbij aan het proberen te vinden van de perfecte tafelindeling voor een enorme bruiloft waarbij elke gast specifieke regels heeft over met wie hij naast mag zitten, of het uitrekenen van het absolute minimum aantal beveiligers dat nodig is om elke hoek van een museum in de gaten te houden zonder een blinde vlek achter te laten.

Een van de beroemdste puzzels in dit veld is het Queen Domination Problem (Koningin-dominantieprobleem). Stel je een schaakbord voor. Een koningin is een machtig stuk dat alles aanvalt in haar rij, haar kolom en beide diagonale paden. De vraag is simpel maar lastig: wat is het kleinste aantal konijnen dat je moet plaatsen op een $n \times n$ bord zodat elk enkel vierkant wordt aangevallen? Het klinkt makkelijk voor een klein bord, maar naarmate het bord groter wordt, explodeert het aantal mogelijke arrangementen naar miljarden, biljoenen en verder. Al meer dan een eeuw proberen wiskundigen dit op te lossen, niet alleen om het aantal te vinden, maar om exact te tellen op hoeveel verschillende manieren je die konijnen kunt plaatsen. Waarom is dit belangrijk? Omdat het oplossen van deze puzzels ons helpt begrijpen hoe we complexe systemen kunnen organiseren, van het plannen van vluchten tot het ontwerpen van computerchips. Maar er is een addertje onder het gras: wanneer computers de wiskunde uitvoeren, kunnen ze fouten maken, en soms missen ze het antwoord volledig.

Dit is waar Taha Rostami en Curtis Bright in beeld komen met hun artikel, "Queen Domination by SAT Solving." Zij pakten het probleem aan van het tellen van alle unieke manieren om het minimale aantal konijnen te plaatsen op schaakborden tot grootte 19. In plaats van een op maat gemaakt programma te schrijven om naar oplossingen te zoeken zoals eerdere onderzoekers deden, vertaalden zij de volledige schaakbordpuzzel naar een taal die een SAT-solver (een super slimme logische machine) begrijpt. Denk aan een SAT-solver als een detective die controleert of een reeks regels ooit waar kan zijn. Als de detective "nee" zegt, kan hij dit bewijzen met een certificaat dat iedereen kan controleren om te verifiëren dat de detective niet heeft gelogen.

De auteurs bouwden een speciale "vertaling" van het schaakbord die de geometrie van het spel benadrukte, waarbij ze een slimme truc gebruikten genaamd een Hilbert-curve om de aanwijzingen te organiseren, zodat de detective het antwoord sneller kon vinden. Ze gebruikten ook een strategie genaamd Cube-and-Conquer, wat lijkt op het opdelen van een gigantische, onmogelijk te eten taart in duizenden kleine, hanteerbare stukjes die verschillende computers tegelijkertijd kunnen eten. Het resultaat? Ze hebben de puzzel niet alleen opgelost; ze bewezen dat hun oplossing 100% correct is.

Hun werk bracht een verrassende fout in de geschiedenis van dit probleem aan het licht. Voor een 16x16 bord dachten eerdere experts dat er slechts 43 unieke manieren waren om de konijnen te plaatsen. Rostami en Bright bewezen dat er eigenlijk 371 manieren zijn—een enorm verschil dat suggereert dat het oude computerprogramma een verborgen bug had waardoor de meeste oplossingen werden gemist. Bovendien losten ze een geval op dat lange tijd openstond: het 19x19 bord. Ze ontdekten dat er precies 11 unieke manieren zijn om dat bord te domineren met het minimale aantal konijnen. Door voor elk resultaat "bewijs-certificaten" te genereren, gaven ze de wiskundige gemeenschap een niveau van vertrouwen dat voorheen onmogelijk was, waarmee ze lieten zien dat wanneer je slimme codering combineert met rigoureuze bewijscontrole, je problemen kunt oplossen die zelfs de beste gespecialiseerde software kunnen missen.

Technische Samenvatting: Queen Domination door SAT-solving

Probleemdefinitie
Het queen domination-probleem zoekt het minimum aantal koninginnen, aangeduid als $\gamma(Q_n)$ , die nodig zijn om elk veld op een $n \times n$ schaakbord aan te vallen. Naast het bepalen van deze minimale waarde, vormt de enumeratie van alle verschillende oplossingen tot isomorfisme (rekening houdend met bordsymmetrieën zoals rotatie en reflectie) een aanzienlijke uitdaging. Hoewel de optimale waarden voor $\gamma(Q_n)$ zijn vastgesteld voor $n \le 25$ met behulp van gespecialiseerde zoekinstrumenten zoals UNIDOM, blijft de enumeratie van niet-isomorfe oplossingen voor grotere borden computationeel intensief. Een kritiek punt van zorg in dit domein is de betrouwbaarheid van computationele resultaten; eerdere discrepanties in andere combinatorische bewijzen (bijv. Lam's probleem) en de ontdekking van bugs in gespecialiseerde solvers benadrukken de noodzaak van onafhankelijk verifieerbare correctheidscertificaten.

Methodologie
De auteurs stellen een bewijs-producerend Boolean Satisfiability (SAT) raamwerk voor om het queen domination-probleem aan te pakken. In plaats van een aangepast zoekalgoritme te implementeren, wordt het probleem gecodeerd in een propositieve formule in Conjunctive Normal Form (CNF). De methodologie rust op verschillende belangrijke technische innovaties:

Lijn-variabele Encoding: De kerninnovatie is de introductie van hulp-Boolean variabelen die representeren of specifieke geometrische lijnen (rijen, kolommen, diagonalen en anti-diagonalen) ten minste één koningin bevatten.
- Koningin-variabelen ( $Q_i$ ): Geven aan of er een koningin op veld $i$ staat.
- Lijn-variabelen ( $L_\ell$ ): Geven aan of lijn $\ell$ "actief" is (een koningin bevat).
- Constraints: Clausules zorgen ervoor dat als een lijn actief is, er een koningin op die lijn bestaat. Dominatie wordt uitgedrukt door te eisen dat voor elk veld ten minste één van de vier snijdende lijnen actief is. Cardinaliteit-constraints beperken het totaal aantal koninginnen ( $\sum Q_i \le \gamma$ ) en het totaal aantal actieve lijnen ( $\sum L_\ell \le 4\gamma$ ).
Cardinality Encoding en Literal Ordering:
- De cardinaliteit-constraints worden gecodeerd met behulp van totalizer-gebaseerde methoden. De koningin-constraint gebruikt een standaard totalizer compatibel met het Cube-and-Conquer framework, terwijl de lijn-constraint een modulo totalizer gebruikt voor prestaties.
- Hilbert Curve Ordering: Een nieuwe strategie voor literal-ordering wordt toegepast op de koningin cardinaliteit-constraint. Door het bord te doorlopen via een Hilbert-curve, worden ruimtelijk aangrenzende velden gegroepeerd in de tellingboom. Dit behoudt de ruimtelijke lokaliteit, wat leidt tot sterkere unit propagation. Experimenten toonden aan dat deze ordening de $n=14$ instantie ongeveer 31,5 keer sneller oploste dan de standaard ordening.
Symmetry Breaking: Om redundante exploratie van symmetrische oplossingen te elimineren, dwingt het raamwerk lexicografische ordening-constraints af (gebaseerd op de methode van Warwick Harvey) tussen de oorspronkelijke koningin-configuratie en haar zeven niet-identieke geometrische transformaties. Dit verminderde de zoektijden aanzienlijk in voorlopige tests (bijv. een 6,64× versnelling voor $n=15$ ).
Cube-and-Conquer: Voor grotere instanties wordt de zoekruimte opgedeeld in onafhankelijke subproblemen (cubes) door te brancheren op hulp-variabelen van de totalizer-encoding. Dit maakt parallel oplossen mogelijk en verbetert de schaalbaarheid zonder afhankelijk te zijn van individuele koningin-plaatsingen voor partitionering.
Bewijsgeneratie en Verificatie: Het raamwerk gebruikt cadical-exhaust om alle modellen te enumereren door iteratief blokkerende clausules toe te voegen. Het genereert DRAT-bewijzen met "trusted clauses" om volledigheid te certificeren. Deze bewijzen worden onafhankelijk geverifieerd met drat-trim-t, wat garandeert dat de resultaten niet afhangen van de interne correctheid van de zoeklogica van de solver, maar alleen van de encoding en de bewijschecker.

Belangrijkste Resultaten
De studie heeft succesvol de niet-isomorfe minimale queen domination oplossingen geënumereerd voor alle $n \le 19$ . De resultaten bevatten:

Correctie van de Literatuur: Voor $n=16$ identificeert het artikel een discrepantie in eerdere rapportages. Terwijl de gespecialiseerde solver UNIDOM 43 niet-isomorfe oplossingen rapporteerde, bewijst het SAT-raamwerk dat er exact 371 zijn. De auteurs schrijven dit toe aan een bug in UNIDOM die ervoor zorgt dat geldige oplossingen worden gemist onder specifieke configuraties.
Resolutie van Open Case: De voorheen openstaande casus van $n=19$ is opgelost, waarbij is vastgesteld dat er exact 11 niet-isomorfe minimale oplossingen zijn.
Prestaties: Het SAT-raamwerk presteerde consequent beter dan de gespecialiseerde solver UNIDOM op niet-triviale instanties. Voor $n=19$ nam de SAT-aanpak ongeveer 171.575 seconden (CPU-tijd) in beslag voor enumeratie, vergeleken met 713.733 seconden voor UNIDOM. De inclusie van lijn-variabelen was cruciaal; een voorlopige versie zonder deze variabelen deed er 22,8 keer langer over om de $n=19$ instantie op te lossen en te verifiëren.

Betekenis en Claims
Het artikel claimt dat de primaire bijdrage een hoog-presterende, onafhankelijk verifieerbare oplossing is voor het queen domination enumeratie-probleem. Door de verschuiving van gespecialiseerde zoekcode naar een bewijs-producerend SAT-raamwerk, verminderen de auteurs de "vertrouwen" die vereist is in het computationele proces. De correctheid van de resultaten hangt nu uitsluitend af van de SAT-encoding en de externe bewijsverifieerder, in plaats van de complexe, custom-geschreven logica van een gespecialiseerde solver.

Het werk demonstreert dat zorgvuldige encoding-ontwerp—specifiek de introductie van hulp-variabelen om geometrische structuur bloot te leggen, het gebruik van globale constraints, en geometrie-bewuste literal-ordering—het mogelijk maakt dat bewijs-producerend SAT-solving competitief is met, en superieur aan, hoog-geoptimaliseerde domeinspecifieke solvers. De auteurs maken hun broncode en oplossing-data publiekelijk beschikbaar om verdere verificatie en onderzoek te faciliteren.

Technische Samenvatting: Queen Domination door SAT-solving

Meer zoals dit