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

ToySolver.SAT.Encoder.PBNLC

Contents

The encoder type
Adding constraints
Linearization

Description

Synopsis

data Encoder m
newEncoder :: AddPBLin m a => a -> Encoder m -> m (Encoder m)
getTseitinEncoder :: Encoder m -> Encoder m
addPBNLAtLeast :: AddPBNL m a => a -> PBSum -> Integer -> m ()
addPBNLAtMost :: AddPBNL m a => a -> PBSum -> Integer -> m ()
addPBNLExactly :: AddPBNL m a => a -> PBSum -> Integer -> m ()
addPBNLAtLeastSoft :: AddPBNL m a => a -> Lit -> PBSum -> Integer -> m ()
addPBNLAtMostSoft :: AddPBNL m a => a -> Lit -> PBSum -> Integer -> m ()
addPBNLExactlySoft :: AddPBNL m a => a -> Lit -> PBSum -> Integer -> m ()
linearizePBSum :: PrimMonad m => Encoder m -> PBSum -> m PBLinSum
linearizePBSumWithPolarity :: PrimMonad m => Encoder m -> Polarity -> PBSum -> m PBLinSum

The encoder type

data Encoder m Source #

Instances

Instances details

Monad m => AddCardinality m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PBNLC 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 #
Instance details Defined in ToySolver.SAT.Encoder.PBNLC Methods addClause :: Encoder m -> Clause -> m () Source #
Monad m => AddPBLin m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PBNLC 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 #
PrimMonad m => AddPBNL m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PBNLC 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 => NewVar m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PBNLC Methods newVar :: Encoder m -> m Var Source # newVars :: Encoder m -> Int -> m [Var] Source # newVars_ :: Encoder m -> Int -> m () Source #

newEncoder :: AddPBLin m a => a -> Encoder m -> m (Encoder m) Source #

getTseitinEncoder :: Encoder m -> Encoder m Source #

Adding constraints

addPBNLAtLeast Source #

Arguments

:: AddPBNL m a
=> a
-> PBSum	List of terms `[(c1,ls1),(c2,ls2),…]`
-> Integer	n
-> m ()

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

addPBNLAtMost Source #

Arguments

:: AddPBNL m a
=> a
-> PBSum	List of terms `[(c1,ls1),(c2,ls2),…]`
-> Integer	n
-> m ()

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

addPBNLExactly Source #

Arguments

:: AddPBNL m a
=> a
-> PBSum	List of terms `[(c1,ls1),(c2,ls2),…]`
-> Integer	n
-> m ()

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

addPBNLAtLeastSoft Source #

Arguments

:: AddPBNL m a
=> a
-> Lit	Selector literal `sel`
-> PBSum	List of terms `[(c1,ls1),(c2,ls2),…]`
-> Integer	n
-> m ()

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

addPBNLAtMostSoft Source #

Arguments

:: AddPBNL m a
=> a
-> Lit	Selector literal `sel`
-> PBSum	List of terms `[(c1,ls1),(c2,ls2),…]`
-> Integer	n
-> m ()

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

addPBNLExactlySoft Source #

Arguments

:: AddPBNL m a
=> a
-> Lit	Selector literal `sel`
-> PBSum	List of terms `[(c1,ls1),(c2,ls2),…]`
-> Integer	n
-> m ()

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

Linearization

linearizePBSum :: PrimMonad m => Encoder m -> PBSum -> m PBLinSum Source #

Encode a non-linear PBSum into a lienar PBLinSum.

linearizePBSum enc s is equivalent to linearizePBSumWithPolarity enc polarityBoth.

linearizePBSumWithPolarity :: PrimMonad m => Encoder m -> Polarity -> PBSum -> m PBLinSum Source #

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.