toysolver-0.3.0: Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc

Copyright(c) Masahiro Sakai 2012
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

ToySolver.SAT.TseitinEncoder

Contents

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éen and N. Sörensson. Translating Pseudo-Boolean Constraints into SAT. JSAT 2:1–26, 2006.

Synopsis

The Encoder type

data Encoder Source

Encoder instance

newEncoder :: Solver -> IO Encoder Source

Create a Encoder instance.

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

Use pseudo boolean constraints or use only clauses.

encSolver :: Encoder -> Solver Source

Polarity

data Polarity Source

Constructors

Polarity 

Fields

polarityPosOccurs :: Bool
 
polarityNegOccurs :: Bool
 

Instances

negatePolarity :: Polarity -> Polarity Source

polarityPos :: Polarity Source

polarityNeg :: Polarity Source

polarityBoth :: Polarity Source

polarityNone :: Polarity Source

Boolean formula type

type Formula = BoolExpr Lit Source

Arbitrary formula not restricted to CNF

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

Encoding of boolean formulas

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.

  encodeConj encoder = encodeConjWithPolarity encoder polarityBoth

encodeConjWithPolarity :: Encoder -> Polarity -> [Lit] -> IO Lit Source

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

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

Return an literal which is equivalent to a given disjunction.

  encodeDisj encoder = encodeDisjWithPolarity encoder polarityBoth

encodeDisjWithPolarity :: Encoder -> Polarity -> [Lit] -> IO Lit Source

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

encodeITE :: Encoder -> Lit -> Lit -> Lit -> IO Lit Source

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

  encodeITE encoder = encodeITEWithPolarity encoder polarityBoth

encodeITEWithPolarity :: Encoder -> Polarity -> Lit -> Lit -> Lit -> IO Lit Source

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

Retrieving definitions

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