De onredelijke effectiviteit van machine learning

SAT solven is simpel gezegd het oplossen van een formule met nulletjes en eentjes. Denk eerst aan een gewone formule met getallen en onbekenden, bijvoorbeeld: a + b = 10.

Iedereen van boven de 8 kan zo een aantal a'tjes en b'tjes verzinnen die daaraan voldoen, bijvoorbeeld a = 2 en b = 8, of wat gekker: a = -117 en b = 127. Niet het eerste waar je aan denkt, maar beide kloppen.

Je kunt zulke formules ook maken met booleans in plaats van getallen. Booleans mogen true of false zijn; soms wordt dat weergegeven als 0 of 1. Bijvoorbeeld deze formule: a of niet b = true. Deze formule kunnen we waar maken door bijvoorbeeld a op true te zetten en b op false. Of a op false en b ook op false. Reken maar na!

Een SAT solver heeft bij een formule alle mogelijke oplossingen voor de variabelen. Dat lijkt op een leuke puzzel voor de hobbyist, maar dit is een zogeheten NP-volledig-probleem, en dus heel moeilijk. Het probleem ligt ook aan de basis van veel praktische toepassingen, zoals het maken van roosters of het ontwerpen van chips.

Veel wetenschappers werken aan dit probleem, zo veel dat er zelfs wedstrijden zijn waarin de verschillende SAT solvers het tegen elkaar opnemen. Heel mooi, want zo stuwen wetenschappers elkaar naar grote hoogte.

Nu deed de vakgroep van Holger iets heel slims, zo slim dat hij niet meer mocht meedoen aan de wedstrijden. In plaats van zelf een algoritme te verzinnen, gebruikte hij een machinelearningalgoritme dat vooraf ging bekijken welke van de bestaande tools uit eerdere jaren het het beste zou doen. Deed de tool het in het verleden goed op bijvoorbeeld een probleem met veel variabelen, dan ging hij die toepassen. Deed een ander algoritme het juist top op kleine testen, dan werd die ingezet op kleine voorbeelden. Voor elk probleem gebruikte hij zo de tool die het waarschijnlijk het beste zou doen. En wat bleek: het werkte geweldig. Zo goed dat hij niet meer mocht meedoen aan de wedstrijd!

Het allermooiste van Holgers resultaten is niet dat zijn algoritme het zo goed deed, maar dat de meeste bestaande SAT solvers wel iets konden bijdragen aan zijn resultaten. Het was niet zo dat hij altijd de top 3-solvers gebruikte; zelfs solvers die onder aan de competitie bungelden waren soms de beste keus. Dat is een mooie boodschap: iedereen kan bijdragen!

Overigens hoeft Holger zich niet te vervelen. Hij is zijn eigen competitie begonnen waar ‘algorithm selectors’ juist van harte welkom zijn.