| Copyright | (c) Masahiro Sakai 2012-2014 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
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
- module ToySolver.SAT.MUS.Types
- data Options = Options {
- optLogger :: String -> IO ()
- optOnMCSFound :: MCS -> IO ()
- optOnMUSFound :: MUS -> IO ()
- optKnownMCSes :: [MCS]
- optKnownMUSes :: [MUS]
- optKnownCSes :: [CS]
- defaultOptions :: Options
- allMCSAssumptions :: Solver -> [Lit] -> Options -> IO [MCS]
- allMUSAssumptions :: Solver -> [Lit] -> Options -> IO [MUS]
- enumMCSAssumptions :: Solver -> [Lit] -> Options -> IO ()
- camus :: Solver -> [Lit] -> Options -> IO ([MUS], [MCS])
Documentation
module ToySolver.SAT.MUS.Types
Options for enumMCSAssumptions, allMCSAssumptions, allMUSAssumptions
Constructors
| Options | |
Fields
| |
defaultOptions :: Options Source
default Options value