toysolver-0.7.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Copyright(c) Masahiro Sakai 2016
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010
Extensions
  • ScopedTypeVariables
  • FlexibleContexts
  • ExplicitForAll

ToySolver.SAT.Encoder.PB.Internal.BDD

Description

  • [ES06] N. Eén and N. Sörensson. Translating Pseudo-Boolean Constraints into SAT. JSAT 2:1–26, 2006.

Documentation

addPBLinAtLeastBDD :: PrimMonad m => Encoder m -> PBLinAtLeast -> m () Source #

encodePBLinAtLeastBDD :: forall m. PrimMonad m => Encoder m -> PBLinAtLeast -> m Lit Source #