| Copyright | (c) Masahiro Sakai 2012-2014 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
ToySolver.SAT.MUS.Types
Description
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
Unsatisfiable Subset of constraints (US).
A subset U ⊆ C is an US if U is unsatisfiable.
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].
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.
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.
Satisfiable Subset (SS).
A subset S ⊆ C is a SS if S is satisfiable.
A SS is the complement of a CS.