toysolver-0.1.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.

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.

Encoding of boolean formula

data Formula Source

Arbitrary formula not restricted to CNF

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.

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

Return an literal which is equivalent to a given disjunction.