toysolver-0.8.1: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Copyright(c) Masahiro Sakai 2018
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010
Extensions
  • MonoLocalBinds
  • BangPatterns
  • TypeFamilies
  • FlexibleContexts
  • KindSignatures
  • ExplicitNamespaces

ToySolver.Converter.NAESAT

Description

Not-All-Equal SAT problems.

Synopsis

Definition of NAE (Not-All-Equall) SAT problems.

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

Show SAT2NAESATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

Eq SAT2NAESATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

BackwardTransformer SAT2NAESATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

ForwardTransformer SAT2NAESATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

Transformer SAT2NAESATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

type Source SAT2NAESATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

type Target SAT2NAESATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

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

Instances details
Read NAESAT2NAEKSATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

Show NAESAT2NAEKSATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

Eq NAESAT2NAEKSATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

BackwardTransformer NAESAT2NAEKSATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

ForwardTransformer NAESAT2NAEKSATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

Transformer NAESAT2NAEKSATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

type Source NAESAT2NAEKSATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

type Target NAESAT2NAEKSATInfo Source # 
Instance details

Defined in ToySolver.Converter.NAESAT

NAE-SAT to MAX-2-SAT