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 a -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

edit
  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 Wikipedia by adding missing information.

📚 Artikel Terkait di Wikipedia

Boolean satisfiability problem

TRUE. If this is the case, the formula is called satisfiable, else unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can

SAT solver

there are possible values of x and y which make the formula true, or unsatisfiable, meaning that there are no such values of x and y. In this case, the

Agda (programming language)

possible constructors have arguments that are unavailable, i.e. they have unsatisfiable premisses. Here no value of type isJust A can be constructed because

First-order logic

show that C ∨ D {\displaystyle C\lor D} is unsatisfiable requires showing that C and D are each unsatisfiable; this corresponds to a branching point in

Waterfall model

design problems may necessitate the removal of conflicting or otherwise unsatisfiable/undesignable requirements).[citation needed] In the same paper Royce

Formal methods

specification, then determining that ¬ P {\displaystyle \neg {\mathcal {P}}} is unsatisfiable is equivalent to determining that all executions conform to the specification

Kleene Award

by Rewriting in the Calculus of Constructions" 2002 Albert Atserias "Unsatisfiable Random Formulas are Hard to Certify" 2003 Benjamin Rossman "Successor-Invariance

Glossary of artificial intelligence

true. The opposites of these concepts are unsatisfiability and invalidity, that is, a formula is unsatisfiable if none of the interpretations make the formula