Portability | portable |
---|---|
Stability | provisional |
Maintainer | masahiro.sakai@gmail.com |
Safe Haskell | None |
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.
The Encoder
type
newEncoder :: Solver -> IO EncoderSource
Create a Encoder
instance.
Encoding of boolean formula
Arbitrary formula not restricted to CNF
addFormula :: Encoder -> Formula -> IO ()Source
Assert a given formula to underlying SAT solver by using Tseitin encoding.