ToySolver.SAT.TseitinEncoder

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

data Encoder

Encoder instance

newEncoder :: Solver -> IO Encoder

Create a Encoder instance.

setUsePB :: Encoder -> Bool -> IO ()

Use pseudo boolean constraints or use only clauses.

encSolver :: Encoder -> Solver

Encoding of boolean formula

data Formula

Arbitrary formula not restricted to CNF

Constructors

Lit Lit

And [Formula]

Or [Formula]

Not Formula

Imply Formula Formula

Equiv Formula Formula

Instances

Eq Formula

Ord Formula

Show Formula

evalFormula :: IModel m => m -> Formula -> Bool

addFormula :: Encoder -> Formula -> IO ()

Assert a given formula to underlying SAT solver by using Tseitin encoding.

encodeConj :: Encoder -> [Lit] -> IO Lit

Return an literal which is equivalent to a given conjunction.

encodeDisj :: Encoder -> [Lit] -> IO Lit

Return an literal which is equivalent to a given disjunction.

getDefinitions :: Encoder -> IO [(Lit, Formula)]