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.