CODEWITHSUNDEEP
algorithmsat
Mario Giambarioli
Mario Giambarioli

Reputation: 101

Minimal unsatisfiable core algorithm

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.

Upvotes: 0

Views: 258

Answers (1)

Max Ostrowski
Max Ostrowski

Reputation: 623

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

Upvotes: 1

Related Questions