Copyright	(c) Masahiro Sakai 20132016-2018
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

ToySolver.Converter.PB

Contents

Normalization of PB/WBO problems
Linealization of PB/WBO problems
Quadratization of PB problems
Converting inequality constraints into equality constraints
Converting constraints into penalty terms in objective function
PB↔WBO conversion
SAT↔PB conversion
MaxSAT↔WBO conversion
PB→QUBO conversion

Description

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 #

normalizeWBO :: SoftFormula -> SoftFormula 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

Eq PBQuadratizeInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods (==) :: PBQuadratizeInfo -> PBQuadratizeInfo -> Bool # (/=) :: PBQuadratizeInfo -> PBQuadratizeInfo -> Bool #
Show PBQuadratizeInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods showsPrec :: Int -> PBQuadratizeInfo -> ShowS # show :: PBQuadratizeInfo -> String # showList :: [PBQuadratizeInfo] -> ShowS #
ObjValueBackwardTransformer PBQuadratizeInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueBackward :: PBQuadratizeInfo -> TargetObjValue PBQuadratizeInfo -> SourceObjValue PBQuadratizeInfo Source #
ObjValueForwardTransformer PBQuadratizeInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueForward :: PBQuadratizeInfo -> SourceObjValue PBQuadratizeInfo -> TargetObjValue PBQuadratizeInfo Source #
ObjValueTransformer PBQuadratizeInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type SourceObjValue PBQuadratizeInfo :: Type Source # type TargetObjValue PBQuadratizeInfo :: Type Source #
BackwardTransformer PBQuadratizeInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformBackward :: PBQuadratizeInfo -> Target PBQuadratizeInfo -> Source PBQuadratizeInfo Source #
ForwardTransformer PBQuadratizeInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformForward :: PBQuadratizeInfo -> Source PBQuadratizeInfo -> Target PBQuadratizeInfo Source #
Transformer PBQuadratizeInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type Source PBQuadratizeInfo :: Type Source # type Target PBQuadratizeInfo :: Type Source #
type SourceObjValue PBQuadratizeInfo Source #
Instance details Defined in ToySolver.Converter.PB type SourceObjValue PBQuadratizeInfo = Integer
type TargetObjValue PBQuadratizeInfo Source #
Instance details Defined in ToySolver.Converter.PB type TargetObjValue PBQuadratizeInfo = Integer
type Source PBQuadratizeInfo Source #
Instance details Defined in ToySolver.Converter.PB type Source PBQuadratizeInfo = Model
type Target PBQuadratizeInfo Source #
Instance details Defined in ToySolver.Converter.PB type Target PBQuadratizeInfo = Model

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

Eq PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods (==) :: PBInequalitiesToEqualitiesInfo -> PBInequalitiesToEqualitiesInfo -> Bool # (/=) :: PBInequalitiesToEqualitiesInfo -> PBInequalitiesToEqualitiesInfo -> Bool #
Show PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods showsPrec :: Int -> PBInequalitiesToEqualitiesInfo -> ShowS # show :: PBInequalitiesToEqualitiesInfo -> String # showList :: [PBInequalitiesToEqualitiesInfo] -> ShowS #
ObjValueBackwardTransformer PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueBackward :: PBInequalitiesToEqualitiesInfo -> TargetObjValue PBInequalitiesToEqualitiesInfo -> SourceObjValue PBInequalitiesToEqualitiesInfo Source #
ObjValueForwardTransformer PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueForward :: PBInequalitiesToEqualitiesInfo -> SourceObjValue PBInequalitiesToEqualitiesInfo -> TargetObjValue PBInequalitiesToEqualitiesInfo Source #
ObjValueTransformer PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type SourceObjValue PBInequalitiesToEqualitiesInfo :: Type Source # type TargetObjValue PBInequalitiesToEqualitiesInfo :: Type Source #
BackwardTransformer PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformBackward :: PBInequalitiesToEqualitiesInfo -> Target PBInequalitiesToEqualitiesInfo -> Source PBInequalitiesToEqualitiesInfo Source #
ForwardTransformer PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformForward :: PBInequalitiesToEqualitiesInfo -> Source PBInequalitiesToEqualitiesInfo -> Target PBInequalitiesToEqualitiesInfo Source #
Transformer PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type Source PBInequalitiesToEqualitiesInfo :: Type Source # type Target PBInequalitiesToEqualitiesInfo :: Type Source #
type SourceObjValue PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB type SourceObjValue PBInequalitiesToEqualitiesInfo = Integer
type TargetObjValue PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB type TargetObjValue PBInequalitiesToEqualitiesInfo = Integer
type Source PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB type Source PBInequalitiesToEqualitiesInfo = Model
type Target PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB type Target PBInequalitiesToEqualitiesInfo = Model

Converting constraints into penalty terms in objective function

unconstrainPB :: Formula -> ((Formula, Integer), PBUnconstrainInfo) Source #

data PBUnconstrainInfo Source #

Instances

Eq PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods (==) :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool # (/=) :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool #
Show PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods showsPrec :: Int -> PBUnconstrainInfo -> ShowS # show :: PBUnconstrainInfo -> String # showList :: [PBUnconstrainInfo] -> ShowS #
ObjValueBackwardTransformer PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueBackward :: PBUnconstrainInfo -> TargetObjValue PBUnconstrainInfo -> SourceObjValue PBUnconstrainInfo Source #
ObjValueForwardTransformer PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueForward :: PBUnconstrainInfo -> SourceObjValue PBUnconstrainInfo -> TargetObjValue PBUnconstrainInfo Source #
ObjValueTransformer PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type SourceObjValue PBUnconstrainInfo :: Type Source # type TargetObjValue PBUnconstrainInfo :: Type Source #
BackwardTransformer PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformBackward :: PBUnconstrainInfo -> Target PBUnconstrainInfo -> Source PBUnconstrainInfo Source #
ForwardTransformer PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformForward :: PBUnconstrainInfo -> Source PBUnconstrainInfo -> Target PBUnconstrainInfo Source #
Transformer PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type Source PBUnconstrainInfo :: Type Source # type Target PBUnconstrainInfo :: Type Source #
type SourceObjValue PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB type SourceObjValue PBUnconstrainInfo = Integer
type TargetObjValue PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB type TargetObjValue PBUnconstrainInfo = Integer
type Source PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB type Source PBUnconstrainInfo = Model
type Target PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB type Target PBUnconstrainInfo = Model

PB↔WBO conversion

pb2wbo :: Formula -> (SoftFormula, PB2WBOInfo) Source #

type PB2WBOInfo = IdentityTransformer Model Source #

wbo2pb :: SoftFormula -> (Formula, WBO2PBInfo) Source #

data WBO2PBInfo Source #

Constructors

WBO2PBInfo !Int !Int [(Var, Constraint)]

Instances

Eq WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods (==) :: WBO2PBInfo -> WBO2PBInfo -> Bool # (/=) :: WBO2PBInfo -> WBO2PBInfo -> Bool #
Show WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods showsPrec :: Int -> WBO2PBInfo -> ShowS # show :: WBO2PBInfo -> String # showList :: [WBO2PBInfo] -> ShowS #
BackwardTransformer WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformBackward :: WBO2PBInfo -> Target WBO2PBInfo -> Source WBO2PBInfo Source #
ForwardTransformer WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformForward :: WBO2PBInfo -> Source WBO2PBInfo -> Target WBO2PBInfo Source #
Transformer WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type Source WBO2PBInfo :: Type Source # type Target WBO2PBInfo :: Type Source #
type Source WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB type Source WBO2PBInfo = Model
type Target WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB type Target WBO2PBInfo = Model

addWBO :: (PrimMonad m, AddPBNL m enc) => enc -> SoftFormula -> m (PBSum, [(Var, Constraint)]) Source #

SAT↔PB conversion

sat2pb :: CNF -> (Formula, SAT2PBInfo) Source #

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 #

type MaxSAT2WBOInfo = IdentityTransformer Model Source #

wbo2maxsat :: SoftFormula -> (WCNF, WBO2MaxSATInfo) Source #

type WBO2MaxSATInfo = TseitinInfo Source #

PB→QUBO conversion

pb2qubo' :: Formula -> ((Formula, Integer), PB2QUBOInfo') Source #

type PB2QUBOInfo' = ComposedTransformer PBUnconstrainInfo PBQuadratizeInfo Source #