Technische Universiteit Delft
Smart Solving
door M&C
Promotie van dhr. M.J.H. Heule: "Smart Solving"
25 maart 2008 | 15:00 uur
plaats: Aula TU Delft
De heer Ir. M.J.H. Heule | informatica ingenieur, Nederland
promotor | Prof.dr. C. Witteveen (EWI)
toeg.prom | Dr. H. van Maaren (UHD-EWI)
Smart Solving
Het vervulbaarheidsprobleem (satisfiability, afgekort SAT) ligt aan de
basis van de complexiteitstheorie. Daarnaast staat SAT steeds meer in
de belangstelling als een effectieve representatie om problemen van
andere aard te lijf te gaan: veel problemen kunnen vertaald worden
naar SAT en middels een programma voor dit probleem (SAT solver)
worden opgelost. Door de toenemende kracht van SAT solvers groeit het
aantal toepassingen ieder jaar. Voorbeelden van toepassingen zijn
hardware- en software-verificatie en tal van wiskundige puzzels. 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.
Het leeuwendeel van de SAT solvers is gebaseerd op architecturen die
door middel van goedkope beslissingen snel de zoekruimte verkennen.
Deze solvers zijn ook zeer succesvol op de SAT competities. Onder het
motivatie "Goedkoop is duurkoop" beschrijft deze thesis twee SAT
solvers gebaseerd op architecturen die bekend staan om hun dure
beslissingen. De filosofie hierachter is dat betere beslissingen de
zoekruimte zo kunnen indammen dat het probleem uiteindelijk sneller
kan worden oplost. Beide architecturen zijn al jaren bekend, maar niet
per definitie geliefd, vanwege de hoge kosten die ermee gepaard gaan.
Door dure beslissingen efficiënt te implementeren en het toevoegen van
nieuwe redeneertechnieken en adaptieve heuristieken zijn deze solvers
krachtiger dan alternatieve solvers gebaseerd op deze architecturen.
Een van onze solvers is zelfs zeer slagvaardig op tal van problemen.
Deze heeft een groot aantal prijzen gewonnen, waaronder twee eerste
prijzen tijdens de SAT 2007 competitie.
Meer informatie?
Voor inzage in proefschriften van de promovendi kunt kijken in de TU
Delft Repository op: repository.tudelft.nl. TU Delft Repository is de
digitale vindplaats van openbare publicaties van de TU Delft.
Proefschriften zullen binnen een paar weken na de desbetreffende
promotie in de Repository te vinden zijn.
Laatst gewijzigd: 28 februari 2008