| Copyright | (c) Masahiro Sakai 2012 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
ToySolver.SAT.TseitinEncoder
Description
Tseitin encoding
TODO:
- reduce variables.
References:
- [Tse83] G. Tseitin. On the complexity of derivation in propositional calculus. Automation of Reasoning: Classical Papers in Computational Logic, 2:466-483, 1983. Springer-Verlag.
- [For60] R. Fortet. Application de l'algèbre de Boole en rechercheop opérationelle. Revue Française de Recherche Opérationelle, 4:17-26, 1960.
- [BM84a] E. Balas and J. B. Mazzola. Nonlinear 0-1 programming: I. Linearization techniques. Mathematical Programming, 30(1):1-21, 1984.
- [BM84b] E. Balas and J. B. Mazzola. Nonlinear 0-1 programming: II. Dominance relations and algorithms. Mathematical Programming, 30(1):22-45, 1984.
- data Encoder
- newEncoder :: Solver -> IO Encoder
- setUsePB :: Encoder -> Bool -> IO ()
- encSolver :: Encoder -> Solver
- type Formula = BoolExpr Lit
- evalFormula :: IModel m => m -> Formula -> Bool
- addFormula :: Encoder -> Formula -> IO ()
- encodeConj :: Encoder -> [Lit] -> IO Lit
- encodeDisj :: Encoder -> [Lit] -> IO Lit
- getDefinitions :: Encoder -> IO [(Lit, Formula)]
The Encoder type
newEncoder :: Solver -> IO Encoder Source
Create a Encoder instance.
Encoding of boolean formula
evalFormula :: IModel m => m -> Formula -> Bool Source
addFormula :: Encoder -> Formula -> IO () Source
Assert a given formula to underlying SAT solver by using Tseitin encoding.
encodeConj :: Encoder -> [Lit] -> IO Lit Source
Return an literal which is equivalent to a given conjunction.