ToySolver.SAT.MUS.DAA

"Dualize and Advance" algorithm for finding minimal unsatisfiable sets.

• [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 Options

Options for enumMCSAssumptions, allMCSAssumptions, allMUSAssumptions

Constructors

Options

Fields

optLogger :: String -> IO ()

optOnMCSFound :: MCS -> IO ()

optOnMUSFound :: MUS -> IO ()

optKnownMCSes :: [MCS]

optKnownMUSes :: [MUS]

optKnownCSes :: [CS]

MCS candidates (see HYCAM paper for details). A MCS candidate must be a superset of a real MCS.

Instances

Default Options

defaultOptions :: Options

default Options value

allMCSAssumptions :: Solver -> [Lit] -> Options -> IO [MCS]

allMUSAssumptions :: Solver -> [Lit] -> Options -> IO [MUS]

daa :: Solver -> [Lit] -> Options -> IO ([MUS], [MCS])