In
mathematical logic
Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
, given an
unsatisfiable
In mathematical logic, a Well-formed formula, formula is ''satisfiable'' if it is true under some assignment of values to its Variable (mathematics), variables. For example, the formula x+3=y is satisfiable because it is true when x=3 and y=6, whil ...
Boolean
propositional formula
In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value. A propositional fo ...
in
conjunctive normal form
In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a can ...
, a subset of clauses whose conjunction is still unsatisfiable is called an unsatisfiable core of the original formula.
Many
SAT solver
The SAT ( ) is a standardized test widely used for college admissions in the United States. Since its debut in 1926, its name and scoring have changed several times; originally called the Scholastic Aptitude Test, it was later called the Schola ...
s 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
In mathematical analysis, the maxima and minima (the respective plurals of maximum and minimum) of a function, known collectively as extrema (the plural of extremum), are the largest and smallest value of the function, either within a given ran ...
, 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 core are known.
Notice the terminology: whereas the ''
minimal unsatisfiable core'' was a local problem with an easy solution, the ''
minimum
In mathematical analysis, the maxima and minima (the respective plurals of maximum and minimum) of a function, known collectively as extrema (the plural of extremum), are the largest and smallest value of the function, either within a given ran ...
unsatisfiable core'' is a global problem with no known easy solution.
References
{{logic-stub
Propositional calculus