a minimum unsatisfiable core is the smallest set of constraints that is unsatisfiable.
When deleting one (not any??), it becomes satisfiable.
The size of a minimal unsatisfiable core is the number of constraints.
The proof that a core is minimal is polynomial (delete one constraint and
give a satisfying assignment. Iterate through all constraints).
Given a type T (a set of relations) what can we say about the minimum unsatisfiable cores
of type T? What is the unsatisfiable core of a symmetric formula?
Compute maximal assignment for formula. Consider satisfiable subformula for maximum assignment.
Add one more constraint => becomes unsat
For game:
raw material is a CSP-formula
Finished product is a minimum unsatisfiable core.
quality of finished product is size of minimum unsat core
just another formulation of the same game.