toysolver-0.3.0: Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc

Copyright(c) Masahiro Sakai 2015
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

ToySolver.SAT.MUS.QuickXplain

Description

Minimal Unsatifiable Subset (MUS) Finder based on QuickXplain algorithm.

References:

Synopsis

Documentation

data Options Source

Options for findMUSAssumptions function

Constructors

Options 

Fields

optLogger :: String -> IO ()
 
optUpdateBest :: [Lit] -> IO ()
 
optLitPrinter :: Lit -> String
 

Instances

findMUSAssumptions :: Solver -> Options -> IO MUS Source

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