Copyright	(c) Masahiro Sakai 2018
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	None
Language	Haskell2010
Extensions	MonoLocalBinds BangPatterns TypeFamilies KindSignatures ExplicitNamespaces

ToySolver.Converter.SAT2MaxSAT

Contents

SAT to Max-2-SAT conversion
Max-2-SAT to simple Max-Cut conversion
SAT to simple Max-Cut conversion
Low-level conversion

Description

M. R. Garey, D. S. Johnson, and L. Stockmeyer. Some simplified NP-complete problems. In STOC ’74: Proceedings of the sixth annual ACM symposium on Theory of computing, pages 47–63, New York, NY, USA, 1974. https://dl.acm.org/citation.cfm?doid=800119.803884 https://www.sciencedirect.com/science/article/pii/0304397576900591

Synopsis

type SATToMaxSAT2Info = ComposedTransformer SAT2KSATInfo SAT3ToMaxSAT2Info
satToMaxSAT2 :: CNF -> ((WCNF, Integer), SATToMaxSAT2Info)
type MaxSAT2ToSimpleMaxCutInfo = ComposedTransformer SimplifyMaxSAT2Info SimpleMaxSAT2ToSimpleMaxCutInfo
maxSAT2ToSimpleMaxCut :: (WCNF, Integer) -> ((Problem Integer, Integer), MaxSAT2ToSimpleMaxCutInfo)
type SATToSimpleMaxCutInfo = ComposedTransformer SATToMaxSAT2Info MaxSAT2ToSimpleMaxCutInfo
satToSimpleMaxCut :: CNF -> ((Problem Integer, Integer), SATToSimpleMaxCutInfo)
data SAT3ToMaxSAT2Info = SAT3ToMaxSAT2Info !Int !Int (IntMap (Lit, Lit, Lit))
sat3ToMaxSAT2 :: CNF -> ((WCNF, Integer), SAT3ToMaxSAT2Info)
type SimpleMaxSAT2 = (Int, Set (Int, Int), Integer)
data SimplifyMaxSAT2Info = SimplifyMaxSAT2Info !Int !Int (IntMap (Lit, Lit))
simplifyMaxSAT2 :: (WCNF, Integer) -> (SimpleMaxSAT2, SimplifyMaxSAT2Info)
data SimpleMaxSAT2ToSimpleMaxCutInfo = SimpleMaxSAT2ToSimpleMaxCutInfo !Int !Int
simpleMaxSAT2ToSimpleMaxCut :: SimpleMaxSAT2 -> ((Problem Integer, Integer), SimpleMaxSAT2ToSimpleMaxCutInfo)

SAT to Max-2-SAT conversion

type SATToMaxSAT2Info = ComposedTransformer SAT2KSATInfo SAT3ToMaxSAT2Info Source #

satToMaxSAT2 :: CNF -> ((WCNF, Integer), SATToMaxSAT2Info) Source #

Max-2-SAT to simple Max-Cut conversion

type MaxSAT2ToSimpleMaxCutInfo = ComposedTransformer SimplifyMaxSAT2Info SimpleMaxSAT2ToSimpleMaxCutInfo Source #

maxSAT2ToSimpleMaxCut :: (WCNF, Integer) -> ((Problem Integer, Integer), MaxSAT2ToSimpleMaxCutInfo) Source #

SAT to simple Max-Cut conversion

type SATToSimpleMaxCutInfo = ComposedTransformer SATToMaxSAT2Info MaxSAT2ToSimpleMaxCutInfo Source #

satToSimpleMaxCut :: CNF -> ((Problem Integer, Integer), SATToSimpleMaxCutInfo) Source #

Low-level conversion

3-SAT to Max-2-SAT conversion

data SAT3ToMaxSAT2Info Source #

Constructors

SAT3ToMaxSAT2Info !Int !Int (IntMap (Lit, Lit, Lit))

Instances

Instances details

Eq SAT3ToMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods (==) :: SAT3ToMaxSAT2Info -> SAT3ToMaxSAT2Info -> Bool # (/=) :: SAT3ToMaxSAT2Info -> SAT3ToMaxSAT2Info -> Bool #
Read SAT3ToMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods readsPrec :: Int -> ReadS SAT3ToMaxSAT2Info # readList :: ReadS [SAT3ToMaxSAT2Info] # readPrec :: ReadPrec SAT3ToMaxSAT2Info # readListPrec :: ReadPrec [SAT3ToMaxSAT2Info] #
Show SAT3ToMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods showsPrec :: Int -> SAT3ToMaxSAT2Info -> ShowS # show :: SAT3ToMaxSAT2Info -> String # showList :: [SAT3ToMaxSAT2Info] -> ShowS #
BackwardTransformer SAT3ToMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods transformBackward :: SAT3ToMaxSAT2Info -> Target SAT3ToMaxSAT2Info -> Source SAT3ToMaxSAT2Info Source #
ForwardTransformer SAT3ToMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods transformForward :: SAT3ToMaxSAT2Info -> Source SAT3ToMaxSAT2Info -> Target SAT3ToMaxSAT2Info Source #
Transformer SAT3ToMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Associated Types type Source SAT3ToMaxSAT2Info Source # type Target SAT3ToMaxSAT2Info Source #
type Source SAT3ToMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT type Source SAT3ToMaxSAT2Info = Model
type Target SAT3ToMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT type Target SAT3ToMaxSAT2Info = Model

sat3ToMaxSAT2 :: CNF -> ((WCNF, Integer), SAT3ToMaxSAT2Info) Source #

Max-2-SAT to SimpleMaxSAT2 conversion

type SimpleMaxSAT2 = (Int, Set (Int, Int), Integer) Source #

data SimplifyMaxSAT2Info Source #

Constructors

SimplifyMaxSAT2Info !Int !Int (IntMap (Lit, Lit))

Instances

Instances details

Eq SimplifyMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods (==) :: SimplifyMaxSAT2Info -> SimplifyMaxSAT2Info -> Bool # (/=) :: SimplifyMaxSAT2Info -> SimplifyMaxSAT2Info -> Bool #
Read SimplifyMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods readsPrec :: Int -> ReadS SimplifyMaxSAT2Info # readList :: ReadS [SimplifyMaxSAT2Info] # readPrec :: ReadPrec SimplifyMaxSAT2Info # readListPrec :: ReadPrec [SimplifyMaxSAT2Info] #
Show SimplifyMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods showsPrec :: Int -> SimplifyMaxSAT2Info -> ShowS # show :: SimplifyMaxSAT2Info -> String # showList :: [SimplifyMaxSAT2Info] -> ShowS #
BackwardTransformer SimplifyMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods transformBackward :: SimplifyMaxSAT2Info -> Target SimplifyMaxSAT2Info -> Source SimplifyMaxSAT2Info Source #
ForwardTransformer SimplifyMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods transformForward :: SimplifyMaxSAT2Info -> Source SimplifyMaxSAT2Info -> Target SimplifyMaxSAT2Info Source #
Transformer SimplifyMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Associated Types type Source SimplifyMaxSAT2Info Source # type Target SimplifyMaxSAT2Info Source #
type Source SimplifyMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT type Source SimplifyMaxSAT2Info = Model
type Target SimplifyMaxSAT2Info Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT type Target SimplifyMaxSAT2Info = Model

simplifyMaxSAT2 :: (WCNF, Integer) -> (SimpleMaxSAT2, SimplifyMaxSAT2Info) Source #

SimpleMaxSAT2 to simple Max-Cut conversion

data SimpleMaxSAT2ToSimpleMaxCutInfo Source #

Constructors

SimpleMaxSAT2ToSimpleMaxCutInfo !Int !Int

Instances

Instances details

Eq SimpleMaxSAT2ToSimpleMaxCutInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods (==) :: SimpleMaxSAT2ToSimpleMaxCutInfo -> SimpleMaxSAT2ToSimpleMaxCutInfo -> Bool # (/=) :: SimpleMaxSAT2ToSimpleMaxCutInfo -> SimpleMaxSAT2ToSimpleMaxCutInfo -> Bool #
Read SimpleMaxSAT2ToSimpleMaxCutInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods readsPrec :: Int -> ReadS SimpleMaxSAT2ToSimpleMaxCutInfo # readList :: ReadS [SimpleMaxSAT2ToSimpleMaxCutInfo] # readPrec :: ReadPrec SimpleMaxSAT2ToSimpleMaxCutInfo # readListPrec :: ReadPrec [SimpleMaxSAT2ToSimpleMaxCutInfo] #
Show SimpleMaxSAT2ToSimpleMaxCutInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods showsPrec :: Int -> SimpleMaxSAT2ToSimpleMaxCutInfo -> ShowS # show :: SimpleMaxSAT2ToSimpleMaxCutInfo -> String # showList :: [SimpleMaxSAT2ToSimpleMaxCutInfo] -> ShowS #
BackwardTransformer SimpleMaxSAT2ToSimpleMaxCutInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods transformBackward :: SimpleMaxSAT2ToSimpleMaxCutInfo -> Target SimpleMaxSAT2ToSimpleMaxCutInfo -> Source SimpleMaxSAT2ToSimpleMaxCutInfo Source #
ForwardTransformer SimpleMaxSAT2ToSimpleMaxCutInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Methods transformForward :: SimpleMaxSAT2ToSimpleMaxCutInfo -> Source SimpleMaxSAT2ToSimpleMaxCutInfo -> Target SimpleMaxSAT2ToSimpleMaxCutInfo Source #
Transformer SimpleMaxSAT2ToSimpleMaxCutInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT Associated Types type Source SimpleMaxSAT2ToSimpleMaxCutInfo Source # type Target SimpleMaxSAT2ToSimpleMaxCutInfo Source #
type Source SimpleMaxSAT2ToSimpleMaxCutInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT type Source SimpleMaxSAT2ToSimpleMaxCutInfo = Model
type Target SimpleMaxSAT2ToSimpleMaxCutInfo Source #
Instance details Defined in ToySolver.Converter.SAT2MaxSAT type Target SimpleMaxSAT2ToSimpleMaxCutInfo = Solution

simpleMaxSAT2ToSimpleMaxCut :: SimpleMaxSAT2 -> ((Problem Integer, Integer), SimpleMaxSAT2ToSimpleMaxCutInfo) Source #