ToySolver.SAT.MUS

Description

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

Synopsis

Documentation

Constructors

Instances details

Bounded Method Source #
Instance details Defined in ToySolver.SAT.MUS.Base Methods minBound :: Method # maxBound :: Method #
Enum Method Source #
Instance details 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] #
Show Method Source #
Instance details Defined in ToySolver.SAT.MUS.Base Methods showsPrec :: Int -> Method -> ShowS # show :: Method -> String # showList :: [Method] -> ShowS #
Eq Method Source #
Instance details Defined in ToySolver.SAT.MUS.Base Methods (==) :: Method -> Method -> Bool # (/=) :: Method -> Method -> Bool #
Ord Method Source #
Instance details 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 #

Options for MUS finding.

The default value can be obtained by def.

Constructors

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 details

Default Options Source #
Instance details Defined in ToySolver.SAT.MUS.Base Methods def :: Options #

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