Unsatisfiable core
{{Short description|Concept in the Boolean satisfiability problem}}
In mathematical logic, given an unsatisfiable Boolean propositional formula in conjunctive normal form, a subset of clauses whose conjunction is still unsatisfiable is called an unsatisfiable core of the original formula.
Many SAT solvers can produce a resolution graph which proves the unsatisfiability of the original problem. This can be analyzed to produce a smaller unsatisfiable core.
An unsatisfiable core is called a minimal unsatisfiable core, if every proper subset (allowing removal of any arbitrary clause or clauses) of it is satisfiable. Thus, such a core is a local minimum, though not necessarily a global one. There are several practical methods of computing minimal unsatisfiable cores.{{cite book |last1=Dershowitz |first1=N. |last2=Hanna |first2=Z. |last3=Nadel |first3=A. |chapter=A Scalable Algorithm for Minimal Unsatisfiable Core Extraction |chapter-url=http://www.cs.tau.ac.il/~nachum/papers/ScalableAlgorithm.pdf |editor1-last=Biere |editor1-first=A. |editor2-last=Gomes |editor2-first=C.P. |title=Theory and Applications of Satisfiability Testing — SAT 2006 |publisher=Springer |series=Lecture Notes in Computer Science |volume=4121 |date=2006 |isbn=978-3-540-37207-3 |pages=36–41 |doi=10.1007/11814948_5 |arxiv=cs/0605085 |citeseerx=10.1.1.101.5209|s2cid=2845982 }}{{cite journal |author1-link=Stefan Szeider |first=Stefan |last=Szeider |title=Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable |journal=Journal of Computer and System Sciences |volume=69 |issue=4 |pages=656–674 |date=December 2004 |doi=10.1016/j.jcss.2004.04.009 |citeseerx=10.1.1.634.5311 |url=}}
A minimum unsatisfiable core contains the smallest number of the original clauses required to still be unsatisfiable. No practical algorithms for computing the minimum unsatisfiable core are known,{{cite journal |last1=Liffiton |first1=M.H. |last2=Sakallah |first2=K.A. |title=Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints |journal=J Autom Reason |volume=40 |issue= |pages=1–33 |date=2008 |doi=10.1007/s10817-007-9084-z |citeseerx=10.1.1.79.1304 |s2cid=11106131 |url=http://www.iwu.edu/~mliffito/publications/jar_liffiton_CAMUS.pdf}} and computing a minimum unsatisfiable core of an input formula in conjunctive normal form is -complete problem.{{Cite web |title=Complexity of computing minimum unsatisfiable core |url=https://cstheory.stackexchange.com/questions/54692/complexity-of-computing-minimum-unsatisfiable-core |access-date=2024-09-24 |website=Theoretical Computer Science Stack Exchange |language=en}} Notice the terminology: whereas the minimal unsatisfiable core was a local problem with an easy solution, the minimum unsatisfiable core is a global problem with no known easy solution.