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.NAESAT
Description
Not-All-Equal SAT problems.
Synopsis
- type NAESAT = (Int, [NAEClause])
- evalNAESAT :: IModel m => m -> NAESAT -> Bool
- type NAEClause = Vector PackedLit
- evalNAEClause :: IModel m => m -> NAEClause -> Bool
- newtype SAT2NAESATInfo = SAT2NAESATInfo Var
- sat2naesat :: CNF -> (NAESAT, SAT2NAESATInfo)
- type NAESAT2SATInfo = IdentityTransformer Model
- naesat2sat :: NAESAT -> (CNF, NAESAT2SATInfo)
- data NAESAT2NAEKSATInfo = NAESAT2NAEKSATInfo !Int !Int [(Var, NAEClause, NAEClause)]
- naesat2naeksat :: Int -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo)
- type NAESAT2Max2SATInfo = ComposedTransformer NAESAT2NAEKSATInfo NAE3SAT2Max2SATInfo
- naesat2max2sat :: NAESAT -> ((WCNF, Integer), NAESAT2Max2SATInfo)
- type NAE3SAT2Max2SATInfo = IdentityTransformer Model
- nae3sat2max2sat :: NAESAT -> ((WCNF, Integer), NAE3SAT2Max2SATInfo)
Definition of NAE (Not-All-Equall) SAT problems.
Conversion with SAT problem
newtype SAT2NAESATInfo Source #
Information of sat2naesat
conversion
Constructors
SAT2NAESATInfo Var |
Instances
sat2naesat :: CNF -> (NAESAT, SAT2NAESATInfo) Source #
Convert a CNF formula φ to an equisatifiable NAE-SAT formula ψ,
together with a SAT2NAESATInfo
type NAESAT2SATInfo = IdentityTransformer Model Source #
Information of naesat2sat
conversion
naesat2sat :: NAESAT -> (CNF, NAESAT2SATInfo) Source #
Convert a NAE-SAT formula φ to an equisatifiable CNF formula ψ,
together with a NAESAT2SATInfo
Conversion from general NAE-SAT to NAE-k-SAT
data NAESAT2NAEKSATInfo Source #
Instances
naesat2naeksat :: Int -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo) Source #
NAE-SAT to MAX-2-SAT
naesat2max2sat :: NAESAT -> ((WCNF, Integer), NAESAT2Max2SATInfo) Source #
nae3sat2max2sat :: NAESAT -> ((WCNF, Integer), NAE3SAT2Max2SATInfo) Source #