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

Copyright(c) Masahiro Sakai 2014
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

ToySolver.SAT.MUS.DAA

Description

"Dualize and Advance" algorithm for finding minimal unsatisfiable sets.

  • [DAA] J. Bailey and P. Stuckey, Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization," in Practical Aspects of Declarative Languages, pp. 174-186, 2005. http://ww2.cs.mu.oz.au/~pjs/papers/padl05.pdf

Synopsis

Documentation

data Options Source

Constructors

Options 

Fields

optLogger :: String -> IO ()
 
optOnMCSFound :: MCS -> IO ()
 
optOnMUSFound :: MUS -> IO ()
 
optKnownMCSes :: [MCS]
 
optKnownMUSes :: [MUS]
 
optKnownCSes :: [CS]

MCS candidates (see HYCAM paper for details). A MCS candidate must be a superset of a real MCS.

Instances

daa :: Solver -> [Lit] -> Options -> IO ([MUS], [MCS]) Source