Een maïspuzzel oplossen met CP-SAT

Het is een fysieke puzzel die bestaat uit een witte "kolf" met groeven en een reeks "maïsstukjes". Elk stukje bestaat uit 3 tot 10 korrels die in een specifieke vorm aan elkaar zitten vastgeplakt en in de groeven kunnen schuiven. Het doel is om ze zo te plaatsen dat ze precies in elkaar passen, zonder overlap en zonder gaten.

Zoals alle software engineers in het jaar des Heren 2026, werd ik snel moe van het zelf oplossen van de puzzel en vroeg ik Claude om het voor me te doen.

Na wat worsteling — het blijkt dat computer vision nog niet helemaal zo goed is, dus ik moest enkele van de vormen van de stukjes verduidelijken — schreef Claude een Python-script dat een oplossing gaf. Het was veel beter dan wat ik zelf zou hebben geschreven, en ik heb er uiteindelijk van geleerd.

Wat ik had verwacht

Als ik dit probleem zelf had opgelost, zou ik naïef hebben gegrepen naar recursive backtracking. Als je programmeur bent, heb je dit algoritme waarschijnlijk gezien in een inleidende cursus informatica.

In feite is het de brute-force aanpak: probeer willekeurig iets, probeer dan iets anders, en ga door tot de puzzel is opgelost. Als je vastloopt en er zijn geen legale zetten meer over, maak je je laatste zet ongedaan en probeer je het vanaf dat punt opnieuw. Als alle zetten vanaf dat punt mislukken, maak je nog een zet ongedaan, enzovoort.

Dit is simpelweg een georganiseerde manier om alle opties te proberen, en het staat enkele mooie optimalisaties toe op basis van de structuur van het probleem. Je kunt bijvoorbeeld rekening houden met de symmetrie (het draaien van de kolf verandert de oplossing niet), of vroegtijdig stoppen als je per ongeluk een enkele korrelruimte isoleert (zodat geen enkel stukje deze meer kan bedekken). Een goed doordachte aanpak van backtracking zou waarschijnlijk werken.

Toen ik echter naar het script van Claude keek, realiseerde ik me vanaf de eerste regel dat ik dom was geweest:

from ortools.sat.python import cp_model

Het wiel is al uitgevonden

In plaats van backtracking importeerde Claude simpelweg een industriële bibliotheek die gemaakt is om dit soort problemen op te lossen: OR-Tools.

CP-SAT is uitgebracht door Google en is bedoeld voor het oplossen van constrained optimization problems (beperkte optimalisatieproblemen), evenals satisfiability problems (vervulbaarheidsproblemen) zoals deze.

Het idee is om elk dergelijk probleem te modelleren als een set variabelen — klassiek binair — en een set beperkingen (constraints) of beweringen over die variabelen die allemaal gelijktijdig moeten worden voldaan. (En een doelfunctie voor optimalisatieproblemen). De bibliotheek maakt vervolgens gebruik van decennia aan onderzoek om efficiënt een instelling voor die variabelen te vinden die aan alle beperkingen voldoet.

Het maïsprobleem is een variant van het Exact Cover probleem, dus kenners kunnen waarschijnlijk al zien hoe dit gerepresenteerd zou worden, maar ik loop erdoorheen omdat het nieuw voor mij was.

De variabelen in dit probleem zijn binair — waar of onwaar — en elke variabele representeert het idee: "Stukje X is op een bepaalde manier geplaatst". Dus voor elke $Ni$ manieren waarop stukje $i$ geplaatst zou kunnen worden, hebben we één variabele $V{i,n}$, die waar ($1$) is als het stukje daar is geplaatst, en onwaar ($0$) als dat niet zo is.

Constraint klasse 1: Alle stukjes worden precies één keer geplaatst

Dit deel is eenvoudig. Voor elk stukje $i$ hebben we:

$$ \sum{n=1}^{Ni} V_{i,n} = 1 $$

Dit dwingt af dat precies één van de $V_{i,n}$ variabelen $1$ is, en de rest $0$.

Constraint klasse 2: Elke plek wordt precies één keer bedekt

Dit is iets lastiger, maar vooral tedious en niet verwarrend. Voor elke plaatsing van een stukje moeten we door alle ruimtes op de kolf gaan die het bedekt en dit toevoegen aan de set van bedekkende stukjes $C_s$. Voor alle ruimtes $s$ op de kolf hebben we vervolgens een zeer vergelijkbare beperking:

$$ \sum{V{i,n} \in Cs} V{i,n} = 1 $$

Zo wordt elk stukje één keer gebruikt en wordt elke plek één keer bedekt. Als we ervan uitgaan dat dit een goed geconstrueerde puzzel is — dus het totale aantal korrels in de stukjes is gelijk aan het aantal ruimtes op de kolf — dan zijn dit alle beperkingen die we nodig hebben.

Het Python-script van Claude om dit op te lossen was vrij ingewikkeld omdat het daadwerkelijk alle mogelijke posities van alle stukjes moest enumereren, maar het aanroepen van de solver zelf was heel straightforward:

for plist in by_piece:
    m.Add(sum(v for v, _ in plist) == 1)
for clist in by_cell:
    m.Add(sum(clist) == 1)
# ...
s.solve(m)

Een handgemaakte CP-SAT aanroeping

Om hier meer over te leren en de les te bevestigen om het wiel niet opnieuw uit te vinden, ben ik bij Recurse samengekomen met Zaki en Tommy om te doen wat waarschijnlijk de meest klassieke toepassing van CP-SAT op een puzzel is: Sudoku.

Dit is een klassieke beginnersapplicatie van de tool en is gemakkelijker toe te passen dan voor de maïspuzzel; we hebben simpelweg één variabele per cel, met een waarde van 1-9, en onze constraint-klassen zijn dat elke rij, kolom en blok elk getal één keer moet hebben.

We hebben geen hulpmethoden nodig om dit op te zetten, zoals de maïspuzzel deed voor het roteren van stukjes:

model_vars = [ [ None for _ in range(9) ] for _ in range(9) ]
for i in range(9):
    for j in range(9):
        board_var_name = f"s[{i},{j}]"
        if board[i][j] == -1:
            model_vars[i][j] = model.new_int_var(1, 9, board_var_name)
        else:
            # voor gegeven waarden is er slechts één legale waarde voor de variabele
            model_vars[i][j] = model.new_int_var(board[i][j], board[i][j], board_var_name)

# rijen
for r in range(9):
    model.add_all_different( [ model_vars[r][c] for c in range(9) ] )

# kolommen
for c in range(9):
    model.add_all_different( [ model_vars[r][c] for r in range(9) ] )

# blokken
for off_r in range(3):
    for off_c in range(3):
        model.add_all_different( [
            model_vars[3*off_r + numpad % 3][3*off_c + numpad // 3]
            for numpad in range(9) ] )

Dit loste inderdaad een referentie-sudoku die we ervoorzagen snel op.

Er is nog veel meer te leren over deze tools, maar we hebben nu het belangrijkste geleerd: wanneer ik in de toekomst weer een probleem tegenkom dat zich leent voor CP-SAT, weet ik dat ik een solver moet proberen en de documentatie moet lezen voor wat ik verder nodig heb, in plaats van het zelf te bouwen.

Links

• Het gesprek met Claude over het oplossen van de maïspuzzel (met het Python-script van Claude)
• Onze Sudoku-solver
• Slides van een korte presentatie die ik hierover gaf bij RC