Development

Software-ontwikkeling
SAT Solver code

De onredelijke effectiviteit van machine learning

Soms zijn AI-toepassingen of hun makers gewoon tè slim.

SAT Solver code © CC BY-SA 2.0 dudka.cz
8 mei 2019

Onlangs was ik op ICT Open – een congres dat wetenschappers en ICT-bedrijven bij elkaar brengt – en daar woonde ik een lezing bij van mijn collega Holger Hoos. Holger werkt aan boolean satifiability solvers (SAT solvers), en een van zijn slimme algoritmes kwam niet door een digitale dopingtest heen. Om te snappen hoe dat zit, moeten we wel eerst even de theorie in!

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.

Magazine AG Connect

Dit artikel is ook gepubliceerd in het magazine van AG Connect (aprilnummer, 2019). Wil je alle artikelen uit dit nummer lezen, klik dan hier voor de inhoudsopgave.

Reactie toevoegen
2
Reacties
Ellert van Koperen 13 mei 2019 13:03

Maar alleen op https, op http doet de site het wel.

Ellert van Koperen 13 mei 2019 13:01

De in het artikel gelinkte 'eigen' satcompetition site veroorzaakt een security waarschuwing en heeft geen content.