# Minimal unsatisfiable core algorithm

Wikipedia says that

There are several practical methods of computing minimal unsatisfiable cores.

but I cannot find any. I suppose that “practical methods” means polynomial algorithms. Be careful, a polynomial algorithm, that finds a minimal unsatisfiable core of a given CNF $$F$$, doesn’t mean that $$P=NP$$, because the algorithm could output a Boolean formula $$G$$ such that if $$F$$ is unsatisfiable, $$G$$ is a minimal unsatisfiable core of $$F$$; if $$F$$ is satisfiable, $$G$$ is a subset of the clauses of $$F$$ 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 wikipedia article litteraly gives you references to do it. Apr 10, 2021 at 12:10
• Yes, but in the reference I didn't found a polynomial algorithm. Apr 10, 2021 at 13:28
• Assuming that "practical" means "polynomial time" seems like it might not be warranted.
– D.W.
Apr 11, 2021 at 7:33
• Could be precise about what problem you want to solve and what your question is? Is the problem: given a CNF formula already known to be unsatisfiable, find a minimal unsatisfiable core? And is your question whether there exists a polynomial-time algorithm?
– D.W.
Apr 11, 2021 at 8:02