Minimal unsatisfiable core algorithm

0
votes

I'm looking for a polynomial algorithm to find a minimal unsatisfiable core of a given CNF formula. In other words, an algorithm that if it inputs a Boolean unsatisfiable CNF, it outputs a subset of the clauses of the given CNF such that they are unsatisfiable and become satisfiable when we remove a clause from the subset. If the give CNF is satisfiable, the algorithm returns a satisfiable subset of the clauses of the given CNF. The algorithm complexity must be polynomial.

1
algorithmsat

1 Answers

1
votes

Given that deciding if a CNF is satisfiable or unsatisfiable is NP-complete (unless P=NP) you will not find a polynomial algorithm for this.

https://en.wikipedia.org/wiki/Conjunctive_normal_form