Many SAT solvers can produce a resolution graph which proves the unsatisfiability of the original problem.
An unsatisfiable core is called a minimal unsatisfiable core, if every proper subset (allowing removal of any arbitrary clause or clauses) of it is satisfiable.
There are several practical methods of computing minimal unsatisfiable cores.
No practical algorithms for computing the minimum unsatisfiable core are known,[3] and computing a minimum unsatisfiable core of an input formula in conjunctive normal form is
[4] Notice the terminology: whereas the minimal unsatisfiable core was a local problem with an easy solution, the minimum unsatisfiable core is a global problem with no known easy solution.