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

ToySolver.SAT.Encoder.PB.Internal.Sorter

Description

References:

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

Documentation

type Base = [Int] Source #

type UDigit = Int Source #

type UNumber = [UDigit] Source #

isRepresentable :: Base -> Integer -> Bool Source #

encode :: Base -> Integer -> UNumber Source #

decode :: Base -> UNumber -> Integer Source #

type Cost = Integer Source #

optimizeBase :: [Integer] -> Base Source #

genSorterCircuit :: Int -> [(Int, Int)] Source #

sortVector :: Ord a => Vector a -> Vector a Source #

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

encodePBLinAtLeastSorter :: PrimMonad m => Encoder m -> PBLinAtLeast -> m Lit Source #