content: -----------------------------------------------------------------------------
  -- |
  -- Module      :  ToySolver.SAT.MUS.Types
  -- Copyright   :  (c) Masahiro Sakai 2012-2014
  -- License     :  BSD-style
  --
  -- Maintainer  :  masahiro.sakai@gmail.com
  -- Stability   :  provisional
  -- Portability :  portable
  --
  -- 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>
  --
  -----------------------------------------------------------------------------
  module ToySolver.SAT.MUS.Types
    ( US
    , MUS
    , CS
    , MCS
    , SS
    , MSS
    ) where
  
  import ToySolver.SAT.Types
  
  -- | Unsatisfiable Subset of constraints (US).
  --
  -- A subset U ⊆ C is an US if U is unsatisfiable.
  type US = 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 MUS = 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 CS = 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 MCS = LitSet
  
  -- | Satisfiable Subset (SS).
  --
  -- A subset S ⊆ C is a SS if S is satisfiable.
  -- A SS is the complement of a 'CS'.
  type SS = 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'.
  type MSS = LitSet
  