ToySolver.SAT.MUS

Minimal Unsatifiable Subset (MUS) Finder

References:

• Ulrich Junker. QuickXplain: Preferred explanations and relaxations for over-constrained problems. In Proc. of AAAI’04, pages 167-172, 2004. http://www.aaai.org/Papers/AAAI/2004/AAAI04-027.pdf

Documentation

module ToySolver.SAT.MUS.Types

data Method

Constructors

Deletion

Insertion

QuickXplain

Instances

Bounded Method

Defined in ToySolver.SAT.MUS.Base

Methods

minBound :: Method

maxBound :: Method

Enum Method

Defined in ToySolver.SAT.MUS.Base

Methods

succ :: Method -> Method

pred :: Method -> Method

toEnum :: Int -> Method

fromEnum :: Method -> Int

enumFrom :: Method -> [Method]

enumFromThen :: Method -> Method -> [Method]

enumFromTo :: Method -> Method -> [Method]

enumFromThenTo :: Method -> Method -> Method -> [Method]

Eq Method

Defined in ToySolver.SAT.MUS.Base

Methods

(==) :: Method -> Method -> Bool

(/=) :: Method -> Method -> Bool

Ord Method

Defined in ToySolver.SAT.MUS.Base

Methods

compare :: Method -> Method -> Ordering

(<) :: Method -> Method -> Bool

(<=) :: Method -> Method -> Bool

(>) :: Method -> Method -> Bool

(>=) :: Method -> Method -> Bool

max :: Method -> Method -> Method

min :: Method -> Method -> Method

Show Method

Defined in ToySolver.SAT.MUS.Base

Methods

showsPrec :: Int -> Method -> ShowS

show :: Method -> String

showList :: [Method] -> ShowS

showMethod :: Method -> String

parseMethod :: String -> Maybe Method

data Options

Options for MUS finding.

The default value can be obtained by def.

Constructors

Options

Fields

• optMethod :: Method
• optLogger :: String -> IO ()
• optShowLit :: Lit -> String
• optEvalConstr :: Model -> Lit -> Bool

  Because each soft constraint C_i is represented as a selector literal l_i together with a hard constraint l_i ⇒ C_i, there are cases that a model assigns false to l_i even though C_i itself is true. This function is used to inform the truth value of the original constraint C_i that corresponds to the selector literal l_i.

• optUpdateBest :: US -> IO ()

Instances

Default Options

Defined in ToySolver.SAT.MUS.Base

Methods

def :: Options

findMUSAssumptions :: Solver -> Options -> IO MUS

Find a minimal set of assumptions that causes a conflict. Initial set of assumptions is taken from getFailedAssumptions.