| Copyright | (c) Masahiro Sakai 2015 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
ToySolver.SAT.PBNLC
Description
- type PBTerm = (Integer, [Lit])
- type PBSum = [PBTerm]
- addPBAtLeast :: Encoder -> PBSum -> Integer -> IO ()
- addPBAtMost :: Encoder -> PBSum -> Integer -> IO ()
- addPBExactly :: Encoder -> PBSum -> Integer -> IO ()
- addPBAtLeastSoft :: Encoder -> Lit -> PBSum -> Integer -> IO ()
- addPBAtMostSoft :: Encoder -> Lit -> PBSum -> Integer -> IO ()
- addPBExactlySoft :: Encoder -> Lit -> PBSum -> Integer -> IO ()
- linearizePBSum :: Encoder -> PBSum -> IO PBLinSum
- linearizePBSumWithPolarity :: Encoder -> Polarity -> PBSum -> IO PBLinSum
- evalPBSum :: IModel m => m -> PBSum -> Integer
Documentation
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.
Linearlization
linearizePBSumWithPolarity :: Encoder -> Polarity -> PBSum -> IO PBLinSum Source
Linearize a non-linear PBSum into a lienar PBLinSum.
The input PBSum is assumed to occur only in specified polarity.
- If
polarityPosOccurspPBLinSumis greater than or equal to the value of originalPBSum. - If
polarityNegOccurspPBLinSumis lesser than or equal to the value of originalPBSum.