ToySolver.SAT.CAMUS

• [CAMUS] M. Liffiton and K. Sakallah, Algorithms for computing minimal unsatisfiable subsets of constraints, Journal of Automated Reasoning, vol. 40, no. 1, pp. 1-33, Jan. 2008. http://sun.iwu.edu/~mliffito/publications/jar_liffiton_CAMUS.pdf
• [HYCAM] A. Gregoire, B. Mazure, and C. Piette, Boosting a complete technique to find MSS and MUS: thanks to a local search oracle, in Proceedings of the 20th international joint conference on Artifical intelligence, ser. IJCAI'07. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 2007, pp. 2300-2305. http://ijcai.org/papers07/Papers/IJCAI07-370.pdf

Documentation

type MUS = [Lit]

Minimal Unsatisfiable Subset of constraints.

type MCS = [Lit]

Minimal Correction Subset of constraints.

data Options

Options for enumMCSAssumptions, allMCSAssumptions, allMUSAssumptions

Constructors

Options

Fields

optLogger :: String -> IO ()

optCallback :: MCS -> IO ()

optMCSCandidates :: [MCS]

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

defaultOptions :: Options

default Options value

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

allMUSAssumptions :: Solver -> [Lit] -> Options -> IO [MUS]

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