Minimal unsatisfiable core algorithm
Be careful, a polynomial algorithm, that finds a minimal unsatisfiable core of a given CNF , doesn’t mean that =, because the algorithm could output a Boolean formula  such that if  is unsatisfiable,  is a minimal unsatisfiable core of ; if  is satisfiable,  is a subset of the clauses of  and it is satisfiable. Therefore, the output of the algorithm is a CNF but we don’t know if it is satisfiable or not.

The basis of this statement seems to be a slight misunderstanding of the UNSAT to MINIMAL UNSATISFIABILITY reduction given in The complexity of facets resolved.  This reduction is not a way to produce an unsat core even if the original formula is unsatisfiable.  What the reduction does is embed the original formula into a new formula carefully crafted such that satisfiability is unaffected but the new formula's CNF clauses no longer overlap in the assignments that they forbid.  Because each clause forbids different assignments and because the formula's clauses cover all possible assignments, removing any one clause is guaranteed to make the result satisfiable, which is the definition of a minimally unsatisfiable formula.  But this new formula is not an unsat core of the original formula and tells you nothing about how to find such a core.  The original formula and the new formula are equisatisfiable and thus are related, but they aren't related in a way useful in finding an unsat core for the original formula.
As for practicality, by this the Wikipedia article means &quot;easily implemented once you have a certificate of unsatisfiability for a given Boolean formula.&quot;  If you already have a tool to generate such a certificate, you can produce an unsat core using a polynomial number of calls to that tool.  If the tool requires exponential-time relative to the size of the formula, then you're still looking at an exponential process to find an unsat core.  But it is just as &quot;practical&quot; as determining whether the formula is unsatisfiable in the first place.