25 mrt. 2008
2 minuten
Informaticus Marijn Heule heeft een programma verbeterd om vervulbaarheidsproblemen op te lossen. Stel je moet heel snel een sleutel vinden in een groot onbekend huis. Wat ga je doen? Dit is een voorbeeld voor een zoekstrategie in een vervulbaarheidsprobleem. Niet de oplossing zelf, maar de vraag of er een oplossing bestaat, binnen een bepaald eisenpakket, […]
Informaticus Marijn Heule heeft een programma verbeterd om vervulbaarheidsproblemen op te lossen. Stel je moet heel snel een sleutel vinden in een groot onbekend huis. Wat ga je doen? Dit is een voorbeeld voor een zoekstrategie in een vervulbaarheidsprobleem. Niet de oplossing zelf, maar de vraag of er een oplossing bestaat, binnen een bepaald eisenpakket, staat centraal. Gisteren promoveerde Heule aan de Technische Universiteit Delft.
Steeds meer problemen kunnen worden vertaald naar een vervulbaarheidsprobleem, ook wel satisfialibility of SAT genaamd. Een SAT-probleem kan via een speciaal programma worden opgelost, de zogenaamde solver. Door het sterker worden van de solvers, neemt het aantal toepassingen voor de programma’s toe. Voorbeelden hiervan zijn roosteringsvraagstukken, soft- en hardware-verificatie en wiskundige puzzels.
Aan de hand van het voorbeeld van de speurtocht naar de sleutel beschrijft Heule in zijn proefschrift de bijdragen die hij leverde aan de verbetering van SAT-programma’s.
SAT-solvers zijn er in twee smaken: compleet en incompleet. De eerste soort kamt systematisch de zoekruimte uit en geeft uitsluitsel of een probleem oplosbaar is. Deze versie kent een goedkope, snelle manier: conflictdriven, waarbij hij bij een doodlopende weg terugkeert naar het punt waar het fout ging en de zoektocht vervolgt. De dure lookahead-solver maakt gebruik van een architectuur die vooruitblikt. Deze neemt dure, tijdrovende beslissingen om de zoekruimte zo klein mogelijk te houden. Incomplete solvers zoeken op de bonnefooi en kunnen op een oplossing stuiten. Ook deze solvers kennen goedkope en dure versies. Het leeuwendeel van de SAT-solvers, binnen de industriële benchmark, is gebaseerd op architecturen die door middel van goedkope beslissingen snel de zoekruimte verkennen.
Heule heeft gefocussed op de ontwikkeling ‘dure’ solvers, met als belangrijkste motivatie: goedkoop is duurkoop. Heule zorgde enerzijds dat de kostbare beslissingen efficiënt worden geïmplementeerd, zodat ze minder duur worden maar wel hun impact op de zoekruimte behouden. Anderzijds heeft hij op deze manier de zoekruimte verder verkleind door de redeneerkracht van de solvers uit te breiden. Al met al zorgt dit dat het probleem sneller opgelost kan worden. Het maakt deze solvers krachtiger dan alternatieve solvers gebaseerd op andere architecturen.
Een belangrijke stimulans in dit vakgebied zijn de jaarlijkse SAT competities, waar state-of-the-art SAT solvers worden getest op een breed spectrum aan problemen. De ontwikkelde solvers binnen het onderzoek van Heule hebben een groot aantal prijzen gewonnen op deze gezaghebbende SAT competities.