| Copyright | (c) Masahiro Sakai 2014 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
ToySolver.SAT.MUS.DAA
Description
"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
- module ToySolver.SAT.MUS.Types
- data Options = Options {
- optLogger :: String -> IO ()
- optOnMCSFound :: MCS -> IO ()
- optOnMUSFound :: MUS -> IO ()
- optKnownMCSes :: [MCS]
- optKnownMUSes :: [MUS]
- optKnownCSes :: [CS]
- allMCSAssumptions :: Solver -> [Lit] -> Options -> IO [MCS]
- allMUSAssumptions :: Solver -> [Lit] -> Options -> IO [MUS]
- daa :: Solver -> [Lit] -> Options -> IO ([MUS], [MCS])
Documentation
module ToySolver.SAT.MUS.Types
Options for enumMCSAssumptions, allMCSAssumptions, allMUSAssumptions
The default value can be obtained by def.
Constructors
| Options | |
Fields
| |