Met zes goede ideeën de combinatorische explosie te lijf

Samen met zijn lotgenoten Joris van Zwieten en Mark Dufour zit hij in de klinisch lege werkkamer van docent dr. Hans van Maaren nog na te glunderen van hun huzarenstukje. Met hun geesteskind zijn de drie TU-studenten geëindigd in de hoogste regionen van een internationale kortebaanwedstrijd voor een bepaald soort computerprogramma, de satisfiability solver.

Een satisfiability solver is een ingewikkeld computerprogramma waarmee de sterke en zwakke punten van, bijvoorbeeld, een digitale schakeling kunnen worden opgespoord. Het ontwerpen van een gecompliceerd ding zoals een processor voor de pc gaat vandaag de dag niet zonder tussenkomst van zo’n solver. Het programma gaat op wiskundig verantwoorde manier na of de aan elkaar geknoopte logische poorten en registers waaruit zo’n processor bestaat werkelijk doen wat ervan wordt verwacht. Het doet dat al wanneer de processor alleen nog maar op de tekentafel bestaat.

Elite

Het maken van satisfiability solvers is een bezigheid voor een kleine elite aan het voorfront van de fundamentele informatica. Eens in het jaar komen enkele tientallen informatici, wiskundigen en elektrotechnici van universiteiten en toonaangevende bedrijven ergens op de wereld bijeen om elkaar met nieuwe foefjes de ogen uit te steken. De meegebrachte programma’s worden aan een reeks meedogenloze tests onderworpen. De software die het snelst chocola weet te maken van de voorgeschotelde proefdata is het best, en de programmeur mag zich winnaar noemen van de bewuste benchmark, zoals zo’n test heet.

Dit jaar vond de wetenschappelijke uitputtingsslag begin mei plaats in het Amerikaanse Cincinnati. Tussen de deelnemende arrivés bewogen zich ineens ook een paar debutanten: de drie studenten uit Delft. Althans: namens de drie was Heule in Cincinnati, samen met docent Van Maaren. Laatstgenoemde moet er nog een beetje om grinniken: ,,Heule was als enige op het symposium in pak.”

Berucht

De term ‘satisfiability’ kan worden vertaald met ‘vervulbaarheid’ en een ‘solver’ is iets dat oplossingen zoekt. Een ‘vervulbaarheidsoplosser’ is in wezen een computerprogramma dat zoekt naar oplossingen van een logische vergelijking. De speurtocht is voltooid als er een oplossing is gevonden, met andere woorden: wanneer de vergelijking is vervuld. De speurtocht is ook voltooid als het programma met zekerheid heeft vastgesteld dat er geen oplossing voor de vergelijking bestaat, óók een vorm van vervulling. Afhankelijk van de context kan dat laatste zelfs het beoogde resultaat zijn.

Het zoeken naar een oplossing hoort bij de beruchte wiskundeproblemen die ‘NP-compleet’worden genoemd. Dat wil zeggen dat er geen andere manier bekend is om ze aan te pakken dan alle mogelijkheden stuk voor stuk te proberen. Dit soort problemen heeft de eigenschap met een toenemend aantal mogelijkheden snel onhanteerbaar te worden, zelfs met inschakeling van de allerkrachtigste computers. Men spreekt wel van de ‘combinatorische explosie’. Een bekend voorbeeld is het probleem van de handelsreiziger: zoek de kortste weg die een reiziger moet afleggen om een aantal steden te bezoeken. Het opstellen van ingewikkelde dienstroosters valt in dezelfde categorie, evenals – en daar gaat het hier om – het oplossen van ingewikkelde logische vergelijkingen. Voor de liefhebber is het een heerlijk probleemgebied met vertakkingen naar allerlei exotische uithoeken van de wiskunde; voor de verknochte programmeur een podium om vele kunstjes te vertonen – want zonder computer hoef je er al helemaal niet aan te beginnen.

Ideeën

De beste ‘vervulbaarheidsoplossers’ zijn ontwikkeld aan de universiteiten in Princeton, Berkeley, Toronto, MIT, Zürich en Swansea, waar door de wol geverfde wetenschappers jaren achtereen bezig zijn met het verder verfijnen van hun aanpak. Maar daar was ineens het team van de drie Delftse studenten.

Bij wijze van tentamen programmeerde het trio een eigen oplosser op basis van een methode die ontwikkeld is door Van Maaren en diens promovendus Warner. Het programma kreeg de naam March en werd geschreven ‘in puur C’, zoals Dufour (23) trots opmerkt. Onder programmeurs wil dat zeggen dat je geen watje bent en bij wijze van spreken met de blote hand programmacode smeedt. Het werden avondlijke, met veel zwarte koffie overgoten sessies op de zevende verdieping van de ITS-toren. ,,We hadden alledrie twee goede ideeën”, aldus Van Zwieten (22), ,,en drie maal twee maakt zes goede ideeën in totaal.”

Certificaat

De zes goede ideeën leidden tot hoge plaatsen op verschillende onderdelen van de competitie in Cincinnati. Bij een van de zes wedstrijden in de tweede ronde (in de categorie All solvers on random benchmarks, volgens Van Maaren de moeilijkste) eindigde de Delftse oplosser op de tweede plaats. ‘March’ deed over een bepaald probleem een minuut en veertig seconden, terwijl sommige gerenommeerde deelnemers er drie kwartier op stonden te zwoegen. Een heus certificaat, vervaardigd op de kleurenprinter en met een spelfout in de naam Marijn (‘Marjin’) getuigt van de Delftse triomf.

Na dit eclatante succes gaan de heren zeker wel door op de ingeslagen weg? Er valt immers vast geld te verdienen op deze nog steeds groeiende markt? Van Zwieten en Dufour reageren wat zuinigjes met een ‘eerst maar eens de studie zien af te maken’. Heule ziet zich zeker verder gaan, zij het eerder als wetenschapper dan als zakenman. Een promotie ziet hij wel zitten, al zou die ook kunnen gaan over een andere kluif die hem bezig houdt: cryptografie.

En wat voor cijfer hebben de drie studenten uiteindelijk gekregen voor het ietwat uit de hand gelopen tentamen? Begeleider Van Maaren (51) krijgt een kleur, want dat is er eerlijk gezegd even bij ingeschoten. Maar hij herstelt zich met verve en deelt ter plaatse een cijfer uit: ,,Een tien natuurlijk. Als je hiervoor geen tien zou krijgen, waarvoor dan wel?”

Drie Delftse studenten drongen vanuit het niets door tot in de hoogste regionen van een programmeerwedstrijd voor gerenommeerde wetenschappers.

Sjaak Priester

,,We hebben het best wel goed gedaan”, is het nuchtere commentaar van Marijn Heule, vijfdejaars informaticastudent. Samen met zijn lotgenoten Joris van Zwieten en Mark Dufour zit hij in de klinisch lege werkkamer van docent dr. Hans van Maaren nog na te glunderen van hun huzarenstukje. Met hun geesteskind zijn de drie TU-studenten geëindigd in de hoogste regionen van een internationale kortebaanwedstrijd voor een bepaald soort computerprogramma, de satisfiability solver.

Een satisfiability solver is een ingewikkeld computerprogramma waarmee de sterke en zwakke punten van, bijvoorbeeld, een digitale schakeling kunnen worden opgespoord. Het ontwerpen van een gecompliceerd ding zoals een processor voor de pc gaat vandaag de dag niet zonder tussenkomst van zo’n solver. Het programma gaat op wiskundig verantwoorde manier na of de aan elkaar geknoopte logische poorten en registers waaruit zo’n processor bestaat werkelijk doen wat ervan wordt verwacht. Het doet dat al wanneer de processor alleen nog maar op de tekentafel bestaat.

Elite

Het maken van satisfiability solvers is een bezigheid voor een kleine elite aan het voorfront van de fundamentele informatica. Eens in het jaar komen enkele tientallen informatici, wiskundigen en elektrotechnici van universiteiten en toonaangevende bedrijven ergens op de wereld bijeen om elkaar met nieuwe foefjes de ogen uit te steken. De meegebrachte programma’s worden aan een reeks meedogenloze tests onderworpen. De software die het snelst chocola weet te maken van de voorgeschotelde proefdata is het best, en de programmeur mag zich winnaar noemen van de bewuste benchmark, zoals zo’n test heet.

Dit jaar vond de wetenschappelijke uitputtingsslag begin mei plaats in het Amerikaanse Cincinnati. Tussen de deelnemende arrivés bewogen zich ineens ook een paar debutanten: de drie studenten uit Delft. Althans: namens de drie was Heule in Cincinnati, samen met docent Van Maaren. Laatstgenoemde moet er nog een beetje om grinniken: ,,Heule was als enige op het symposium in pak.”

Berucht

De term ‘satisfiability’ kan worden vertaald met ‘vervulbaarheid’ en een ‘solver’ is iets dat oplossingen zoekt. Een ‘vervulbaarheidsoplosser’ is in wezen een computerprogramma dat zoekt naar oplossingen van een logische vergelijking. De speurtocht is voltooid als er een oplossing is gevonden, met andere woorden: wanneer de vergelijking is vervuld. De speurtocht is ook voltooid als het programma met zekerheid heeft vastgesteld dat er geen oplossing voor de vergelijking bestaat, óók een vorm van vervulling. Afhankelijk van de context kan dat laatste zelfs het beoogde resultaat zijn.

Het zoeken naar een oplossing hoort bij de beruchte wiskundeproblemen die ‘NP-compleet’worden genoemd. Dat wil zeggen dat er geen andere manier bekend is om ze aan te pakken dan alle mogelijkheden stuk voor stuk te proberen. Dit soort problemen heeft de eigenschap met een toenemend aantal mogelijkheden snel onhanteerbaar te worden, zelfs met inschakeling van de allerkrachtigste computers. Men spreekt wel van de ‘combinatorische explosie’. Een bekend voorbeeld is het probleem van de handelsreiziger: zoek de kortste weg die een reiziger moet afleggen om een aantal steden te bezoeken. Het opstellen van ingewikkelde dienstroosters valt in dezelfde categorie, evenals – en daar gaat het hier om – het oplossen van ingewikkelde logische vergelijkingen. Voor de liefhebber is het een heerlijk probleemgebied met vertakkingen naar allerlei exotische uithoeken van de wiskunde; voor de verknochte programmeur een podium om vele kunstjes te vertonen – want zonder computer hoef je er al helemaal niet aan te beginnen.

Ideeën

De beste ‘vervulbaarheidsoplossers’ zijn ontwikkeld aan de universiteiten in Princeton, Berkeley, Toronto, MIT, Zürich en Swansea, waar door de wol geverfde wetenschappers jaren achtereen bezig zijn met het verder verfijnen van hun aanpak. Maar daar was ineens het team van de drie Delftse studenten.

Bij wijze van tentamen programmeerde het trio een eigen oplosser op basis van een methode die ontwikkeld is door Van Maaren en diens promovendus Warner. Het programma kreeg de naam March en werd geschreven ‘in puur C’, zoals Dufour (23) trots opmerkt. Onder programmeurs wil dat zeggen dat je geen watje bent en bij wijze van spreken met de blote hand programmacode smeedt. Het werden avondlijke, met veel zwarte koffie overgoten sessies op de zevende verdieping van de ITS-toren. ,,We hadden alledrie twee goede ideeën”, aldus Van Zwieten (22), ,,en drie maal twee maakt zes goede ideeën in totaal.”

Certificaat

De zes goede ideeën leidden tot hoge plaatsen op verschillende onderdelen van de competitie in Cincinnati. Bij een van de zes wedstrijden in de tweede ronde (in de categorie All solvers on random benchmarks, volgens Van Maaren de moeilijkste) eindigde de Delftse oplosser op de tweede plaats. ‘March’ deed over een bepaald probleem een minuut en veertig seconden, terwijl sommige gerenommeerde deelnemers er drie kwartier op stonden te zwoegen. Een heus certificaat, vervaardigd op de kleurenprinter en met een spelfout in de naam Marijn (‘Marjin’) getuigt van de Delftse triomf.

Na dit eclatante succes gaan de heren zeker wel door op de ingeslagen weg? Er valt immers vast geld te verdienen op deze nog steeds groeiende markt? Van Zwieten en Dufour reageren wat zuinigjes met een ‘eerst maar eens de studie zien af te maken’. Heule ziet zich zeker verder gaan, zij het eerder als wetenschapper dan als zakenman. Een promotie ziet hij wel zitten, al zou die ook kunnen gaan over een andere kluif die hem bezig houdt: cryptografie.

En wat voor cijfer hebben de drie studenten uiteindelijk gekregen voor het ietwat uit de hand gelopen tentamen? Begeleider Van Maaren (51) krijgt een kleur, want dat is er eerlijk gezegd even bij ingeschoten. Maar hij herstelt zich met verve en deelt ter plaatse een cijfer uit: ,,Een tien natuurlijk. Als je hiervoor geen tien zou krijgen, waarvoor dan wel?”