Copyright	(c) Masahiro Sakai 2015
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable (ExistentialQuantification, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses)
Safe Haskell	None
Language	Haskell2010

ToySolver.SAT.Encoder.PBNLC

Contents

Description

Synopsis

The encoder type

Instances

PrimMonad m => AddPBNL m (Encoder m) Source #
Methods addPBNLAtLeast :: Encoder m -> PBSum -> Integer -> m () Source # addPBNLAtMost :: Encoder m -> PBSum -> Integer -> m () Source # addPBNLExactly :: Encoder m -> PBSum -> Integer -> m () Source # addPBNLAtLeastSoft :: Encoder m -> Lit -> PBSum -> Integer -> m () Source # addPBNLAtMostSoft :: Encoder m -> Lit -> PBSum -> Integer -> m () Source # addPBNLExactlySoft :: Encoder m -> Lit -> PBSum -> Integer -> m () Source #
Monad m => AddPBLin m (Encoder m) Source #
Methods addPBAtLeast :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBAtMost :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBExactly :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBAtLeastSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source # addPBAtMostSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source # addPBExactlySoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source #
Monad m => AddCardinality m (Encoder m) Source #
Methods addAtLeast :: Encoder m -> [Lit] -> Int -> m () Source # addAtMost :: Encoder m -> [Lit] -> Int -> m () Source # addExactly :: Encoder m -> [Lit] -> Int -> m () Source #
Monad m => AddClause m (Encoder m) Source #
Methods addClause :: Encoder m -> Clause -> m () Source #
Monad m => NewVar m (Encoder m) Source #
Methods newVar :: Encoder m -> m Var Source # newVars :: Encoder m -> Int -> m [Var] Source # newVars_ :: Encoder m -> Int -> m () Source #

Adding constraints

Add a non-linear pseudo boolean constraints c1*ls1 + c2*ls2 + … ≥ n.

Add a non-linear pseudo boolean constraints c1*ls1 + c2*ls2 + … ≥ n.

Add a non-linear pseudo boolean constraints c1*ls1 + c2*ls2 + … = n.

Add a soft non-linear pseudo boolean constraints sel ⇒ c1*ls1 + c2*ls2 + … ≥ n.

Add a soft non-linear pseudo boolean constraints sel ⇒ c1*ls1 + c2*ls2 + … ≤ n.

Add a soft non-linear pseudo boolean constraints lit ⇒ c1*ls1 + c2*ls2 + … = n.

Encode a non-linear PBSum into a lienar PBLinSum.

linearizePBSum enc s is equivalent to linearizePBSumWithPolarity enc polarityBoth.

Linearize a non-linear PBSum into a lienar PBLinSum.

The input PBSum is assumed to occur only in specified polarity.

If polarityPosOccurs p, the value of resulting PBLinSum is greater than or equal to the value of original PBSum.
If polarityNegOccurs p, the value of resulting PBLinSum is lesser than or equal to the value of original PBSum.