# 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

## 1 Answer

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 "easily implemented once you have a certificate of unsatisfiability for a given Boolean formula." 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 "practical" as determining whether the formula is unsatisfiable in the first place.

• Ok, but in my opinion the Wikipedia article should say "if P=NP, then there are several practical methods of computing minimal unsatisfiable cores". In fact, at the moment, there are no ways to find a minimal unsatisfiable core in polynomial time. Apr 11, 2021 at 15:43
• @MarioGiambarioli, Wikipedia not a primary source and it is not an authoritative reference. I imagine you can always edit it to improve it! But complaining here won't do any good, as we're not responsible for the text there.
– D.W.
Apr 12, 2021 at 3:38