Print Email Facebook Twitter Minimally Unsatisfiable Subformulae Title Minimally Unsatisfiable Subformulae Author Mijnders, S. Contributor Heule, M.J.H. (mentor) Faculty Electrical Engineering, Mathematics and Computer Science Department Software Technology Programme Algorithmics Date 2012-08-13 Abstract Minimal unsatis?ability is a topic in the ?eld of satis?ability (SAT). Minimally unsatis?able subformulae (MUSes) are minimal subsets of an unsatis?able formula that are unsatis?able. They can therefore be seen as causes of unsatis?ability. With recent improvements in SAT solving, extracting MUSes has also become faster. Lately increasingly more effort has been put in getting MUS extraction to industrial strength. This thesis tries to speed up MUS extraction by applying preprocessing techniques from the ?eld of SAT solving. Application is not always straightforward. Some techniques have to be modi?ed and some are not applicable at all. For each of the discussed techniques, this thesis describes how they affect MUSes and what has been done to apply them. Subject MUSsatisfiabilitySATminimal unsatisfiabilityMUS extractionpreprocessingclause eliminationBCPSCCEminimally unsatisfiable subformulaheuristicsself-subsumptionminisatmuser To reference this document use: http://resolver.tudelft.nl/uuid:c7b566fb-387d-4f3a-9553-d59bddc6771d Embargo date 2012-08-15 Part of collection Student theses Document type master thesis Rights (c) 2012 Mijnders, S. Files PDF thesis.pdf 819.39 KB Close viewer /islandora/object/uuid:c7b566fb-387d-4f3a-9553-d59bddc6771d/datastream/OBJ/view