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

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

ToySolver.SAT.MUS.CAMUS

Description

In this module, we assume each soft constraint C_i is represented as a literal. If a constraint C_i is not a literal, we can represent it as a fresh variable v together with a hard constraint v ⇒ C_i.

References:

  • [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

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

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