ToySolver.SAT.Encoder.PB

References:

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

Documentation

data Encoder m

Instances

PrimMonad m => AddPBLin m (Encoder m)

Defined in ToySolver.SAT.Encoder.PB

Methods

addPBAtLeast :: Encoder m -> PBLinSum -> Integer -> m ()

addPBAtMost :: Encoder m -> PBLinSum -> Integer -> m ()

addPBExactly :: Encoder m -> PBLinSum -> Integer -> m ()

addPBAtLeastSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m ()

addPBAtMostSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m ()

addPBExactlySoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m ()

PrimMonad m => AddCardinality m (Encoder m)

Defined in ToySolver.SAT.Encoder.PB

Methods

addAtLeast :: Encoder m -> [Lit] -> Int -> m ()

addAtMost :: Encoder m -> [Lit] -> Int -> m ()

addExactly :: Encoder m -> [Lit] -> Int -> m ()

Monad m => AddClause m (Encoder m)

Defined in ToySolver.SAT.Encoder.PB

Methods

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

Monad m => NewVar m (Encoder m)

Defined in ToySolver.SAT.Encoder.PB

Methods

newVar :: Encoder m -> m Var

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

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

data Strategy

Constructors

BDD

Adder

Sorter

Hybrid

Instances

Bounded Strategy

Defined in ToySolver.SAT.Encoder.PB

Methods

minBound :: Strategy

maxBound :: Strategy

Enum Strategy

Defined in ToySolver.SAT.Encoder.PB

Methods

succ :: Strategy -> Strategy

pred :: Strategy -> Strategy

toEnum :: Int -> Strategy

fromEnum :: Strategy -> Int

enumFrom :: Strategy -> [Strategy]

enumFromThen :: Strategy -> Strategy -> [Strategy]

enumFromTo :: Strategy -> Strategy -> [Strategy]

enumFromThenTo :: Strategy -> Strategy -> Strategy -> [Strategy]

Eq Strategy

Defined in ToySolver.SAT.Encoder.PB

Methods

(==) :: Strategy -> Strategy -> Bool

(/=) :: Strategy -> Strategy -> Bool

Ord Strategy

Defined in ToySolver.SAT.Encoder.PB

Methods

compare :: Strategy -> Strategy -> Ordering

(<) :: Strategy -> Strategy -> Bool

(<=) :: Strategy -> Strategy -> Bool

(>) :: Strategy -> Strategy -> Bool

(>=) :: Strategy -> Strategy -> Bool

max :: Strategy -> Strategy -> Strategy

min :: Strategy -> Strategy -> Strategy

Show Strategy

Defined in ToySolver.SAT.Encoder.PB

Methods

showsPrec :: Int -> Strategy -> ShowS

show :: Strategy -> String

showList :: [Strategy] -> ShowS

Default Strategy

Defined in ToySolver.SAT.Encoder.PB

Methods

def :: Strategy

newEncoder :: Monad m => Encoder m -> m (Encoder m)

newEncoderWithStrategy :: Monad m => Encoder m -> Strategy -> m (Encoder m)

encodePBLinAtLeast :: forall m. PrimMonad m => Encoder m -> PBLinAtLeast -> m Lit