Safe Haskell	None
Language	Haskell2010

ToySolver.Converter.SAT2MIS

Contents

SAT to independent set problem conversion
3-SAT to independent set problem conversion
Maximum independent problem to MaxSAT/PB problem conversion

Synopsis

satToIS :: CNF -> ((Graph, Int), SAT2ISInfo)
type SAT2ISInfo = ComposedTransformer SAT2KSATInfo SAT3ToISInfo
sat3ToIS :: CNF -> ((Graph, Int), SAT3ToISInfo)
data SAT3ToISInfo
is2pb :: (Graph, Int) -> (Formula, IS2SATInfo)
mis2MaxSAT :: Graph -> (WCNF, IS2SATInfo)
data IS2SATInfo

SAT to independent set problem conversion

satToIS :: CNF -> ((Graph, Int), SAT2ISInfo) Source #

type SAT2ISInfo = ComposedTransformer SAT2KSATInfo SAT3ToISInfo Source #

3-SAT to independent set problem conversion

sat3ToIS :: CNF -> ((Graph, Int), SAT3ToISInfo) Source #

data SAT3ToISInfo Source #

Instances

Instances details

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

Maximum independent problem to MaxSAT/PB problem conversion

is2pb :: (Graph, Int) -> (Formula, IS2SATInfo) Source #

mis2MaxSAT :: Graph -> (WCNF, IS2SATInfo) Source #

data IS2SATInfo Source #

Instances

Instances details

Eq IS2SATInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MIS Methods (==) :: IS2SATInfo -> IS2SATInfo -> Bool # (/=) :: IS2SATInfo -> IS2SATInfo -> Bool #
Read IS2SATInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MIS Methods readsPrec :: Int -> ReadS IS2SATInfo # readList :: ReadS [IS2SATInfo] # readPrec :: ReadPrec IS2SATInfo # readListPrec :: ReadPrec [IS2SATInfo] #
Show IS2SATInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MIS Methods showsPrec :: Int -> IS2SATInfo -> ShowS # show :: IS2SATInfo -> String # showList :: [IS2SATInfo] -> ShowS #
ObjValueBackwardTransformer IS2SATInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MIS Methods transformObjValueBackward :: IS2SATInfo -> TargetObjValue IS2SATInfo -> SourceObjValue IS2SATInfo Source #
ObjValueForwardTransformer IS2SATInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MIS Methods transformObjValueForward :: IS2SATInfo -> SourceObjValue IS2SATInfo -> TargetObjValue IS2SATInfo Source #
ObjValueTransformer IS2SATInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MIS Associated Types type SourceObjValue IS2SATInfo Source # type TargetObjValue IS2SATInfo Source #
BackwardTransformer IS2SATInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MIS Methods transformBackward :: IS2SATInfo -> Target IS2SATInfo -> Source IS2SATInfo Source #
ForwardTransformer IS2SATInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MIS Methods transformForward :: IS2SATInfo -> Source IS2SATInfo -> Target IS2SATInfo Source #
Transformer IS2SATInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MIS Associated Types type Source IS2SATInfo Source # type Target IS2SATInfo Source #
type SourceObjValue IS2SATInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MIS type SourceObjValue IS2SATInfo = Int
type TargetObjValue IS2SATInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MIS type TargetObjValue IS2SATInfo = Integer
type Source IS2SATInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MIS type Source IS2SATInfo = IntSet
type Target IS2SATInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MIS type Target IS2SATInfo = Model