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	MonoLocalBinds BangPatterns TypeFamilies FlexibleContexts KindSignatures ExplicitNamespaces

ToySolver.Converter.NAESAT

Contents

Definition of NAE (Not-All-Equall) SAT problems.
Conversion with SAT problem
Conversion from general NAE-SAT to NAE-k-SAT
- NAE-SAT to MAX-2-SAT

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.

type NAESAT = (Int, [NAEClause]) Source #

evalNAESAT :: IModel m => m -> NAESAT -> Bool Source #

type NAEClause = Vector PackedLit Source #

evalNAEClause :: IModel m => m -> NAEClause -> Bool Source #

Conversion with SAT problem

newtype SAT2NAESATInfo Source #

Information of sat2naesat conversion

Constructors

SAT2NAESATInfo Var

Instances

Instances details

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

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 #

Constructors

NAESAT2NAEKSATInfo !Int !Int [(Var, NAEClause, NAEClause)]

Instances

Instances details

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

naesat2naeksat :: Int -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo) Source #

NAE-SAT to MAX-2-SAT

type NAESAT2Max2SATInfo = ComposedTransformer NAESAT2NAEKSATInfo NAE3SAT2Max2SATInfo Source #

naesat2max2sat :: NAESAT -> ((WCNF, Integer), NAESAT2Max2SATInfo) Source #

type NAE3SAT2Max2SATInfo = IdentityTransformer Model Source #

nae3sat2max2sat :: NAESAT -> ((WCNF, Integer), NAE3SAT2Max2SATInfo) Source #