Unsatisfiable core

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.[1][2]

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,[3] and computing a minimum unsatisfiable core of an input formula in conjunctive normal form is ${\displaystyle \Sigma _{2}^{\mathsf {P}}}$-complete problem.[4] 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.

References

1. Dershowitz, N.; Hanna, Z.; Nadel, A. (2006). "A Scalable Algorithm for Minimal Unsatisfiable Core Extraction" (PDF). In Biere, A.; Gomes, C.P. (eds.). Theory and Applications of Satisfiability Testing — SAT 2006. Lecture Notes in Computer Science. Vol. 4121. Springer. pp. 36–41. arXiv:cs/0605085. CiteSeerX 10.1.1.101.5209. doi:10.1007/11814948_5. ISBN 978-3-540-37207-3. S2CID 2845982.
2. Szeider, Stefan (December 2004). "Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable". Journal of Computer and System Sciences. 69 (4): 656–674. CiteSeerX 10.1.1.634.5311. doi:10.1016/j.jcss.2004.04.009.
3. Liffiton, M.H.; Sakallah, K.A. (2008). "Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints" (PDF). J Autom Reason. 40: 1–33. CiteSeerX 10.1.1.79.1304. doi:10.1007/s10817-007-9084-z. S2CID 11106131.
4. "Complexity of computing minimum unsatisfiable core". Theoretical Computer Science Stack Exchange. Retrieved 2024-09-24.