|
| CARD, a cardinality constraints based solver |
 |
|
| NWO, open competitie |
|
|
Abstract (NL) Het Satisfiability onderzoek richt zich op het automatisch oplossen van problemen die zich
binnen de zgn propositielogica laten formuleren. Dit lijkt een beperkt gebied, maar het is bekend dat veel
moeilijke combinatorische problemen als zodanig herformuleerbaar zijn. Satisfiability staat dan ook centraal
in disciplines als Discrete Wiskunde, Hard- en Software verificatie, Ontwerpen en Testen van Elektronische
Schakelingen en er zijn zelfs intrigerende connecties met de Statistische Fysica. Ofschoon, zoals eerder
vermeld, veel combinatorische problemen zich binnen de propositielogica laten herformuleren moet gezegd
worden dat deze herformuleringen in veel gevallen niet "natuurlijk" zijn en er is daarom behoefte ruimere
modelerings mogelijkheden te onderzoeken. Het voorgestelde project wil toegesneden algoritmiek ontwikkelen
voor die problemen die zich laten formuleren via eenvoudige Boolse ongelijkheden. De kunst bestaat
vervolgens hierin dat getracht moet worden zoveel mogelijk van de data structuur optimalisaties en
eenvoudige redeneertechnieken die er zijn voor de basis Satisfiability oplosmethoden te behouden. Alleen dan
komt het oplossen van ( zeer ) grootschalige problemen binnen handbereik.
|
|
|
|
|
Project
