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

Portabilityportable
Stabilityprovisional
Maintainermasahiro.sakai@gmail.com
Safe HaskellNone

SAT.CAMUS

Description

 

Synopsis

Documentation

type MUS = [Lit]Source

type MCS = [Lit]Source

data Options Source

Options for enumMCSAssumptions, allMCSAssumptions, allMUSAssumptions

Constructors

Options 

Fields

optLogger :: String -> IO ()
 
optCallback :: MCS -> IO ()
 

defaultOptions :: OptionsSource

default Options value

allMCSAssumptions :: Solver -> [Lit] -> Options -> IO [MCS]Source

allMUSAssumptions :: Solver -> [Lit] -> Options -> IO [MCS]Source

enumMCSAssumptions :: Solver -> [Lit] -> Options -> IO ()Source

hittingSetDual :: [MCS] -> [MUS]Source