MaxSAT and Minimally Unsatisfiable Subformulas (Cores) [2]

Now we start for minimal unsatisfiable subformulas (MUSes) which I categorize unsatisfiability driven as given in the first post. They are sometimes called as minimal unsatisfiable cores in the literature. I believe the research on computing MUSes made the relation between explanations and relaxations (relaxations in short) in CSP research more prominent. I can not say that one triggered/inspired the other as I do not have enough chronological information...

Explanations and Relaxations in CSP
Relaxations[1] are used to explain the reasons (culprits) of inconsistencies and to (optimally) resolve those inconsistencies in over-constrained CSP problems. Given a CSP problem with a set of user constraints C and background constraints B (hard constraints),  explanations and relaxations are sets of constraints CE ⊆ ℘C and CR ⊆ ℘C respectively. An explanation R ∈ CE is (subset) minimal if the following conditions hold:

• R = {ci, ... , cn} is unsatisfiable 
• Removal of a constraint c from R is satisfiable, i.e. R \ {c} is consistent.

Notice that a subset minimal explanation is not cardinality minimal explanation. A cardinality minimal explanation is a subset minimal explanation that the minimum number of constraints. A relaxation R ∈ CR is a maximal relaxation if the following conditions hold:

• R = {ci,...,cn} is satisfiable 
• Addition of a constraint c to R makes the formula unsatisfiable, i.e. let c ∉ R, the formula R ∪ c is inconsistent.

In very short terms, the relation between explanations and relaxations is the following: the complement of each hitting set of all minimal relaxations is one maximal relaxation. A constructive way of computing explanations is to check the consistency of B ∪ C and iteratively remove one constraint until an unconsistency is obtained. Thus relaxations are computed first. More details are available at [1].

We stop here with CSP explanations and relaxations and start with SAT MUSes in the next post...


References:
[1] Ulrich Junker, "QUICKXPLAIN: Preferred Explanations and Relaxations for Over-Constrained Problems", Proceedings of the Nineteenth National Conference on Artificial Intelligence (AAAI), 2004