ToySolver.SAT.MUS.Types

In this module, we assume each soft constraint C_i is represented as a literal. If a constraint C_i is not a literal, we can represent it as a fresh variable v together with a hard constraint v ⇒ C_i.

References:

• [CAMUS] M. Liffiton and K. Sakallah, Algorithms for computing minimal unsatisfiable subsets of constraints, Journal of Automated Reasoning, vol. 40, no. 1, pp. 1-33, Jan. 2008. http://sun.iwu.edu/~mliffito/publications/jar_liffiton_CAMUS.pdf

Documentation

type US = LitSet

Unsatisfiable Subset of constraints (US).

A subset U ⊆ C is an US if U is unsatisfiable.

type MUS = LitSet

Minimal Unsatisfiable Subset of constraints (MUS).

A subset U ⊆ C is an MUS if U is unsatisfiable and ∀C_i ∈ U, U\{C_i} is satisfiable [CAMUS].

type CS = LitSet

Correction Subset of constraints (CS).

A subset M ⊆ C is a CS if C\M is satisfiable. A CS is the complement of a SS.

type MCS = LitSet

Minimal Correction Subset of constraints (MCS).

A subset M ⊆ C is an MCS if C\M is satisfiable and ∀C_i ∈ M, C\(M\{C_i}) is unsatisfiable [CAMUS]. A MCS is the complement of an MSS and also known as a CoMSS.

type SS = LitSet

Satisfiable Subset (SS).

A subset S ⊆ C is a SS if S is satisfiable. A SS is the complement of a CS.

type MSS = LitSet

Maximal Satisfiable Subset (MSS).

A subset S ⊆ C is an MSS if S is satisfiable and ∀C_i ∈ U\S, S∪{C_i} is unsatisfiable [CAMUS]. A MSS is the complement of an MCS.