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

Satisfiability

as Gödel's completeness theorem. The negation of satisfiability is unsatisfiability, and the negation of validity is invalidity. These four concepts are

Method of analytic tableaux

conjunction is proved to be unsatisfiable. If all conjunctions are proved unsatisfiable, the original set of formulae is unsatisfiable. Every tableau can be

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

Tautology (logic)

a tautology is a formula whose negation is unsatisfiable. In other words, it cannot be false. Unsatisfiable statements, both through negation and affirmation

Davis–Putnam algorithm

an unsatisfiable formula has an unsatisfiable ground instance, and on the fact that a formula is valid if and only if its negation is unsatisfiable. Taken

Local consistency

by some algorithms. Constraint propagation can also be used as an unsatisfiability checker, incomplete in general but complete in some particular cases

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

Constraint logic programming

in a set called the constraint store. If this set is found out to be unsatisfiable, the interpreter backtracks, trying to use other clauses for proving