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 OverloadedStrings FlexibleContexts KindSignatures ExplicitNamespaces

ToySolver.Converter.NAESAT

Contents

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

FromJSON SAT2NAESATInfo Source #

Instance details

Defined in ToySolver.Converter.NAESAT

Methods

parseJSON :: Value -> Parser SAT2NAESATInfo #

parseJSONList :: Value -> Parser [SAT2NAESATInfo] #

omittedField :: Maybe SAT2NAESATInfo #

ToJSON SAT2NAESATInfo Source #

Instance details

Defined in ToySolver.Converter.NAESAT

Methods

toJSON :: SAT2NAESATInfo -> Value #

toEncoding :: SAT2NAESATInfo -> Encoding #

toJSONList :: [SAT2NAESATInfo] -> Value #

toEncodingList :: [SAT2NAESATInfo] -> Encoding #

omitField :: SAT2NAESATInfo -> Bool #

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
Instance details Defined in ToySolver.Converter.NAESAT type Source SAT2NAESATInfo = Model
type Target SAT2NAESATInfo
Instance details Defined in ToySolver.Converter.NAESAT type Target SAT2NAESATInfo = Model

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 equisatisfiable 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 equisatisfiable 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

FromJSON NAESAT2NAEKSATInfo Source #

Instance details

Defined in ToySolver.Converter.NAESAT

Methods

parseJSON :: Value -> Parser NAESAT2NAEKSATInfo #

parseJSONList :: Value -> Parser [NAESAT2NAEKSATInfo] #

omittedField :: Maybe NAESAT2NAEKSATInfo #

ToJSON NAESAT2NAEKSATInfo Source #

Instance details

Defined in ToySolver.Converter.NAESAT

Methods

toJSON :: NAESAT2NAEKSATInfo -> Value #

toEncoding :: NAESAT2NAEKSATInfo -> Encoding #

toJSONList :: [NAESAT2NAEKSATInfo] -> Value #

toEncodingList :: [NAESAT2NAEKSATInfo] -> Encoding #

omitField :: NAESAT2NAEKSATInfo -> Bool #

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
Instance details Defined in ToySolver.Converter.NAESAT type Source NAESAT2NAEKSATInfo = Model
type Target NAESAT2NAEKSATInfo
Instance details Defined in ToySolver.Converter.NAESAT type Target NAESAT2NAEKSATInfo = Model

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 #