Copyright | (c) Masahiro Sakai 20132016-2018 |
---|---|
License | BSD-style |
Maintainer | masahiro.sakai@gmail.com |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Synopsis
- module ToySolver.Converter.Base
- module ToySolver.Converter.Tseitin
- normalizePB :: Formula -> Formula
- normalizeWBO :: SoftFormula -> SoftFormula
- linearizePB :: Formula -> Bool -> (Formula, PBLinearizeInfo)
- linearizeWBO :: SoftFormula -> Bool -> (SoftFormula, PBLinearizeInfo)
- type PBLinearizeInfo = TseitinInfo
- quadratizePB :: Formula -> ((Formula, Integer), PBQuadratizeInfo)
- quadratizePB' :: (Formula, Integer) -> ((Formula, Integer), PBQuadratizeInfo)
- data PBQuadratizeInfo
- inequalitiesToEqualitiesPB :: Formula -> (Formula, PBInequalitiesToEqualitiesInfo)
- data PBInequalitiesToEqualitiesInfo
- unconstrainPB :: Formula -> ((Formula, Integer), PBUnconstrainInfo)
- data PBUnconstrainInfo
- pb2wbo :: Formula -> (SoftFormula, PB2WBOInfo)
- type PB2WBOInfo = IdentityTransformer Model
- wbo2pb :: SoftFormula -> (Formula, WBO2PBInfo)
- data WBO2PBInfo = WBO2PBInfo !Int !Int [(Var, Constraint)]
- addWBO :: (PrimMonad m, AddPBNL m enc) => enc -> SoftFormula -> m (PBSum, [(Var, Constraint)])
- sat2pb :: CNF -> (Formula, SAT2PBInfo)
- type SAT2PBInfo = IdentityTransformer Model
- pb2sat :: Formula -> (CNF, PB2SATInfo)
- type PB2SATInfo = TseitinInfo
- maxsat2wbo :: WCNF -> (SoftFormula, MaxSAT2WBOInfo)
- type MaxSAT2WBOInfo = IdentityTransformer Model
- wbo2maxsat :: SoftFormula -> (WCNF, WBO2MaxSATInfo)
- type WBO2MaxSATInfo = TseitinInfo
- pb2qubo' :: Formula -> ((Formula, Integer), PB2QUBOInfo')
- type PB2QUBOInfo' = ComposedTransformer PBUnconstrainInfo PBQuadratizeInfo
Documentation
module ToySolver.Converter.Base
module ToySolver.Converter.Tseitin
Normalization of PB/WBO problems
normalizePB :: Formula -> Formula Source #
Linealization of PB/WBO problems
linearizePB :: Formula -> Bool -> (Formula, PBLinearizeInfo) Source #
linearizeWBO :: SoftFormula -> Bool -> (SoftFormula, PBLinearizeInfo) Source #
type PBLinearizeInfo = TseitinInfo Source #
Quadratization of PB problems
quadratizePB :: Formula -> ((Formula, Integer), PBQuadratizeInfo) Source #
Quandratize PBO/PBS problem without introducing additional constraints.
quadratizePB' :: (Formula, Integer) -> ((Formula, Integer), PBQuadratizeInfo) Source #
Quandratize PBO/PBS problem without introducing additional constraints.
data PBQuadratizeInfo Source #
Instances
Converting inequality constraints into equality constraints
inequalitiesToEqualitiesPB :: Formula -> (Formula, PBInequalitiesToEqualitiesInfo) Source #
Convert inequality constraints into equality constraints by introducing surpass variables.
data PBInequalitiesToEqualitiesInfo Source #
Instances
Converting constraints into penalty terms in objective function
unconstrainPB :: Formula -> ((Formula, Integer), PBUnconstrainInfo) Source #
data PBUnconstrainInfo Source #
Instances
PB↔WBO conversion
pb2wbo :: Formula -> (SoftFormula, PB2WBOInfo) Source #
type PB2WBOInfo = IdentityTransformer Model Source #
wbo2pb :: SoftFormula -> (Formula, WBO2PBInfo) Source #
data WBO2PBInfo Source #
WBO2PBInfo !Int !Int [(Var, Constraint)] |
Instances
Eq WBO2PBInfo Source # | |
Defined in ToySolver.Converter.PB (==) :: WBO2PBInfo -> WBO2PBInfo -> Bool # (/=) :: WBO2PBInfo -> WBO2PBInfo -> Bool # | |
Show WBO2PBInfo Source # | |
Defined in ToySolver.Converter.PB showsPrec :: Int -> WBO2PBInfo -> ShowS # show :: WBO2PBInfo -> String # showList :: [WBO2PBInfo] -> ShowS # | |
BackwardTransformer WBO2PBInfo Source # | |
Defined in ToySolver.Converter.PB | |
ForwardTransformer WBO2PBInfo Source # | |
Defined in ToySolver.Converter.PB | |
Transformer WBO2PBInfo Source # | |
Defined in ToySolver.Converter.PB type Source WBO2PBInfo :: Type Source # type Target WBO2PBInfo :: Type Source # | |
type Source WBO2PBInfo Source # | |
Defined in ToySolver.Converter.PB | |
type Target WBO2PBInfo Source # | |
Defined in ToySolver.Converter.PB |
addWBO :: (PrimMonad m, AddPBNL m enc) => enc -> SoftFormula -> m (PBSum, [(Var, Constraint)]) Source #
SAT↔PB conversion
type SAT2PBInfo = IdentityTransformer Model Source #
pb2sat :: Formula -> (CNF, PB2SATInfo) Source #
Convert a pseudo boolean formula φ to a equisatisfiable CNF formula ψ together with two functions f and g such that:
- if M ⊨ φ then f(M) ⊨ ψ
- if M ⊨ ψ then g(M) ⊨ φ
type PB2SATInfo = TseitinInfo Source #
MaxSAT↔WBO conversion
maxsat2wbo :: WCNF -> (SoftFormula, MaxSAT2WBOInfo) Source #
wbo2maxsat :: SoftFormula -> (WCNF, WBO2MaxSATInfo) Source #
type WBO2MaxSATInfo = TseitinInfo Source #