ToySolver.SAT.PBNLC

Documentation

type PBTerm = (Integer, [Lit])

type PBSum = [PBTerm]

Adding constraints

addPBAtLeast

Arguments

:: Encoder

-> PBSum

[(c1,ls1),(c2,ls2),…]

-> Integer

n

-> IO ()

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

addPBAtMost

Arguments

:: Encoder

-> PBSum

[(c1,ls1),(c2,ls2),…]

-> Integer

n

-> IO ()

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

addPBExactly

Arguments

:: Encoder

-> PBSum

[(c1,ls1),(c2,ls2),…]

-> Integer

n

-> IO ()

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

addPBAtLeastSoft

Arguments

:: Encoder

-> Lit

Selector literal sel

-> PBSum

[(c1,ls1),(c2,ls2),…]

-> Integer

n

-> IO ()

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

addPBAtMostSoft

Arguments

:: Encoder

-> Lit

Selector literal sel

-> PBSum

[(c1,ls1),(c2,ls2),…]

-> Integer

n

-> IO ()

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

addPBExactlySoft

Arguments

:: Encoder

-> Lit

indicator lit

-> PBSum

[(c1,ls1),(c2,ls2),…]

-> Integer

n

-> IO ()

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

Linearlization

linearizePBSum :: Encoder -> PBSum -> IO PBLinSum

Encode a non-linear PBSum into a lienar PBLinSum.

linearizePBSum enc s is equivalent to linearizePBSumWithPolarity enc polarityBoth.

linearizePBSumWithPolarity :: Encoder -> Polarity -> PBSum -> IO PBLinSum

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.

Evaluation

evalPBSum :: IModel m => m -> PBSum -> Integer