ToySolver.SAT.Encoder.Tseitin

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.
• [PG86] D. Plaisted and S. Greenbaum. A Structure-preserving Clause Form Translation. In Journal on Symbolic Computation, volume 2, 1986.
• [ES06] N. Eén and N. Sörensson. Translating Pseudo-Boolean Constraints into SAT. JSAT 2:1–26, 2006.

The Encoder type

data Encoder m

Encoder instance

Instances

Monad m => AddClause m (Encoder m)

Defined in ToySolver.SAT.Encoder.Tseitin

Methods

addClause :: Encoder m -> Clause -> m ()

Monad m => NewVar m (Encoder m)

Defined in ToySolver.SAT.Encoder.Tseitin

Methods

newVar :: Encoder m -> m Var

newVars :: Encoder m -> Int -> m [Var]

newVars_ :: Encoder m -> Int -> m ()

newEncoder :: PrimMonad m => AddClause m a => a -> m (Encoder m)

Create a Encoder instance. If the encoder is built using this function, setUsePB has no effect.

newEncoderWithPBLin :: PrimMonad m => AddPBLin m a => a -> m (Encoder m)

Create a Encoder instance. If the encoder is built using this function, setUsePB has an effect.

setUsePB :: PrimMonad m => Encoder m -> Bool -> m ()

Use pseudo boolean constraints or use only clauses. This option has an effect only when the encoder is built using newEncoderWithPBLin.

Polarity

data Polarity

Constructors

Polarity

Fields

• polarityPosOccurs :: Bool
• polarityNegOccurs :: Bool

Instances

Eq Polarity

Defined in ToySolver.SAT.Encoder.Tseitin

Methods

(==) :: Polarity -> Polarity -> Bool

(/=) :: Polarity -> Polarity -> Bool

Show Polarity

Defined in ToySolver.SAT.Encoder.Tseitin

Methods

showsPrec :: Int -> Polarity -> ShowS

show :: Polarity -> String

showList :: [Polarity] -> ShowS

negatePolarity :: Polarity -> Polarity

polarityPos :: Polarity

polarityNeg :: Polarity

polarityBoth :: Polarity

polarityNone :: Polarity

Boolean formula type

type Formula = BoolExpr Lit

Arbitrary formula not restricted to CNF

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

Encoding of boolean formulas

addFormula :: PrimMonad m => Encoder m -> Formula -> m ()

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

encodeFormula :: PrimMonad m => Encoder m -> Formula -> m Lit

encodeFormulaWithPolarity :: PrimMonad m => Encoder m -> Polarity -> Formula -> m Lit

encodeConj :: PrimMonad m => Encoder m -> [Lit] -> m Lit

Return an literal which is equivalent to a given conjunction.

  encodeConj encoder = encodeConjWithPolarity encoder polarityBoth

encodeConjWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> [Lit] -> m Lit

Return an literal which is equivalent to a given conjunction which occurs only in specified polarity.

encodeDisj :: PrimMonad m => Encoder m -> [Lit] -> m Lit

Return an literal which is equivalent to a given disjunction.

  encodeDisj encoder = encodeDisjWithPolarity encoder polarityBoth

encodeDisjWithPolarity :: PrimMonad m => Encoder m -> Polarity -> [Lit] -> m Lit

Return an literal which is equivalent to a given disjunction which occurs only in specified polarity.

encodeITE :: PrimMonad m => Encoder m -> Lit -> Lit -> Lit -> m Lit

Return an literal which is equivalent to a given if-then-else.

  encodeITE encoder = encodeITEWithPolarity encoder polarityBoth

encodeITEWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit

Return an literal which is equivalent to a given if-then-else which occurs only in specified polarity.

encodeXOR :: PrimMonad m => Encoder m -> Lit -> Lit -> m Lit

Return an literal which is equivalent to an XOR of given two literals.

  encodeXOR encoder = encodeXORWithPolarity encoder polarityBoth

encodeXORWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> Lit -> Lit -> m Lit

Return an literal which is equivalent to an XOR of given two literals which occurs only in specified polarity.

encodeFASum :: forall m. PrimMonad m => Encoder m -> Lit -> Lit -> Lit -> m Lit

Return an "sum"-pin of a full-adder.

  encodeFASum encoder = encodeFASumWithPolarity encoder polarityBoth

encodeFASumWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit

Return an "sum"-pin of a full-adder which occurs only in specified polarity.

encodeFACarry :: forall m. PrimMonad m => Encoder m -> Lit -> Lit -> Lit -> m Lit

Return an "carry"-pin of a full-adder.

  encodeFACarry encoder = encodeFACarryWithPolarity encoder polarityBoth

encodeFACarryWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit

Return an "carry"-pin of a full-adder which occurs only in specified polarity.

Retrieving definitions

getDefinitions :: PrimMonad m => Encoder m -> m [(Var, Formula)]