| Copyright | (c) Masahiro Sakai 2018 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | non-portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
| Extensions |
|
ToySolver.Converter.SAT2MaxSAT
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)
- type SAT3ToMaxSAT2Info = TseitinInfo
- sat3ToMaxSAT2 :: CNF -> ((WCNF, Integer), SAT3ToMaxSAT2Info)
- type SimpleMaxSAT2 = (Int, Set (Int, Int), Integer)
- type SimplifyMaxSAT2Info = TseitinInfo
- simplifyMaxSAT2 :: (WCNF, Integer) -> (SimpleMaxSAT2, SimplifyMaxSAT2Info)
- data SimpleMaxSAT2ToSimpleMaxCutInfo = SimpleMaxSAT2ToSimpleMaxCutInfo !Int !Int
- simpleMaxSAT2ToSimpleMaxCut :: SimpleMaxSAT2 -> ((Problem Integer, Integer), SimpleMaxSAT2ToSimpleMaxCutInfo)
SAT to Max-2-SAT conversion
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
type SAT3ToMaxSAT2Info = TseitinInfo Source #
sat3ToMaxSAT2 :: CNF -> ((WCNF, Integer), SAT3ToMaxSAT2Info) Source #
Max-2-SAT to SimpleMaxSAT2 conversion
type SimplifyMaxSAT2Info = TseitinInfo Source #
simplifyMaxSAT2 :: (WCNF, Integer) -> (SimpleMaxSAT2, SimplifyMaxSAT2Info) Source #
SimpleMaxSAT2 to simple Max-Cut conversion
data SimpleMaxSAT2ToSimpleMaxCutInfo Source #
Constructors
| SimpleMaxSAT2ToSimpleMaxCutInfo !Int !Int |