A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
scientific article; zbMATH DE number 5633630