| Copyright | (c) Masahiro Sakai 2015 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | non-portable |
| Safe Haskell | None |
| Language | Haskell2010 |
ToySolver.SAT.MUS.QuickXplain
Description
Minimal Unsatifiable Subset (MUS) Finder based on QuickXplain algorithm.
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
- module ToySolver.SAT.MUS.Types
- data Options = Options {
- optLogger :: String -> IO ()
- optUpdateBest :: [Lit] -> IO ()
- optLitPrinter :: Lit -> String
- defaultOptions :: Options
- findMUSAssumptions :: Solver -> Options -> IO MUS
Documentation
module ToySolver.SAT.MUS.Types
Options for findMUSAssumptions function
Constructors
| Options | |
Fields
| |
defaultOptions :: Options Source
default Options value
findMUSAssumptions :: Solver -> Options -> IO MUS Source
Find a minimal set of assumptions that causes a conflict.
Initial set of assumptions is taken from getFailedAssumptions.