toysolver-0.9.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Copyright(c) Masahiro Sakai 2012
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010
Extensions
  • ScopedTypeVariables
  • TypeSynonymInstances
  • FlexibleInstances
  • ConstrainedClassMethods
  • MultiParamTypeClasses
  • ExistentialQuantification
  • ExplicitForAll

ToySolver.SAT.Encoder.Tseitin

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.
  • [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.
Synopsis

The Encoder type

data Encoder m Source #

Encoder instance

Instances

Instances details
Monad m => AddClause m (Encoder m) Source # 
Instance details

Defined in ToySolver.SAT.Encoder.Tseitin

Methods

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

Monad m => NewVar m (Encoder m) Source # 
Instance details

Defined in ToySolver.SAT.Encoder.Tseitin

Methods

newVar :: Encoder m -> m Var Source #

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

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

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

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) Source #

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

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

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

Polarity

data Polarity Source #

Constructors

Polarity 

Fields

Instances

Instances details
Show Polarity Source # 
Instance details

Defined in ToySolver.SAT.Encoder.Tseitin

Methods

showsPrec :: Int -> Polarity -> ShowS #

show :: Polarity -> String #

showList :: [Polarity] -> ShowS #

Eq Polarity Source # 
Instance details

Defined in ToySolver.SAT.Encoder.Tseitin

Methods

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

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

negatePolarity :: Polarity -> Polarity Source #

polarityPos :: Polarity Source #

polarityNeg :: Polarity Source #

polarityBoth :: Polarity Source #

polarityNone :: Polarity Source #

Boolean formula type

module ToySolver.SAT.Formula

Encoding of boolean formulas

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

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

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

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

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

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 Source #

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

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

Return an literal which is equivalent to a given disjunction.

  encodeDisj encoder = encodeDisjWithPolarity encoder polarityBoth

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

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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

Retrieving definitions

getDefinitions :: PrimMonad m => Encoder m -> m (VarMap Formula) Source #