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 core are known.[3] 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
- ↑ Dershowitz, N.; Hanna, Z.; Nadel, A. (2006). "A Scalable Algorithm for Minimal Unsatisfiable Core Extraction". in Biere, A.; Gomes, C.P.. Theory and Applications of Satisfiability Testing — SAT 2006. Lecture Notes in Computer Science. 4121. Springer. pp. 36–41. doi:10.1007/11814948_5. ISBN 978-3-540-37207-3. http://www.cs.tau.ac.il/~nachum/papers/ScalableAlgorithm.pdf.
- ↑ 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. doi:10.1016/j.jcss.2004.04.009.
- ↑ Liffiton, M.H.; Sakallah, K.A. (2008). "Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints". J Autom Reason 40: 1–33. doi:10.1007/s10817-007-9084-z. http://www.iwu.edu/~mliffito/publications/jar_liffiton_CAMUS.pdf.
 |  |
