Minimally Unsatisfiable Subformulae

Master thesis (2012)

Authors

S. Mijnders

Contributors

M.J.H. Heule (mentor)

Programme

Algorithmics () (TU Delft)

Heuristics SAT Satisfiability MUS Minimal unsatisfiability MUS extraction Preprocessing Clause elimination BCP SCCE Minimally unsatisfiable subformula Self-subsumption Minisat Muser

To reference this document use:

http://resolver.tudelft.nl/uuid:c7b566fb-387d-4f3a-9553-d59bddc6771d

More Info

expand_more

Published Date

13-08-2012

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Programme

Algorithmics

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.

Files

Thesis.pdf

(pdf | 0.8 Mb)