Copyright	(c) Masahiro Sakai 2012-2016
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable (MultiParamTypeClasses)
Safe Haskell	None
Language	Haskell2010

ToySolver.SAT.MUS.Enum

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
[HYCAM] A. Gregoire, B. Mazure, and C. Piette, Boosting a complete technique to find MSS and MUS: thanks to a local search oracle, in Proceedings of the 20th international joint conference on Artifical intelligence, ser. IJCAI'07. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 2007, pp. 2300-2305. http://ijcai.org/papers07/Papers/IJCAI07-370.pdf
[DAA] J. Bailey and P. Stuckey, Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization," in Practical Aspects of Declarative Languages, pp. 174-186, 2005. http://ww2.cs.mu.oz.au/~pjs/papers/padl05.pdf

Documentation

module ToySolver.SAT.MUS.Types

data Method Source #

Constructors

CAMUS
DAA
MARCO
GurvichKhachiyan1999

Instances

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

showMethod :: Method -> String Source #

parseMethod :: String -> Maybe Method Source #

data Options Source #

Constructors

Options

Fields

optMethod :: Method
optLogger :: String -> IO ()
optShowLit :: Lit -> String
MCS candidates (see HYCAM paper for details). A MCS candidate must be a superset of a real MCS.
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.
optOnMCSFound :: MCS -> IO ()
optOnMUSFound :: MUS -> IO ()
optKnownMCSes :: [MCS]
optKnownMUSes :: [MUS]
optKnownCSes :: [CS]

Instances

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

allMUSAssumptions :: Solver -> [Lit] -> Options -> IO ([MUS], [MCS]) Source #