Misplaced Pages

Unsatisfiable core

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
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.

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

This logic-related article is a stub. You can help Misplaced Pages by expanding it.

Categories: