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

Portabilitynon-portable
Stabilityprovisional
Maintainermasahiro.sakai@gmail.com
Safe HaskellNone

SAT.MUS

Description

Minimal Unsatifiable Subset (MUS) Finder

Synopsis

Documentation

data Options Source

Options for findMUSAssumptions function

Constructors

Options 

Fields

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

findMUSAssumptions :: Solver -> Options -> IO [Lit]Source

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