ToySolver.SAT.MUS.QuickXplain

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

Documentation

module ToySolver.SAT.MUS.Types

data Options

Options for findMUSAssumptions function

The default value can be obtained by def.

Constructors

Options

Fields

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

Instances

Default Options

Methods

def :: Options

findMUSAssumptions :: Solver -> Options -> IO MUS

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