Copyright | (c) Masahiro Sakai 2016-2018 |
---|---|
License | BSD-style |
Maintainer | masahiro.sakai@gmail.com |
Stability | provisional |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Reader and Writer for DIMACS CNF and family of similar formats.
Synopsis
- module ToySolver.FileFormat.Base
- data CNF = CNF {
- cnfNumVars :: !Int
- cnfNumClauses :: !Int
- cnfClauses :: [PackedClause]
- data WCNF = WCNF {
- wcnfNumVars :: !Int
- wcnfNumClauses :: !Int
- wcnfTopCost :: !Weight
- wcnfClauses :: [WeightedClause]
- type WeightedClause = (Weight, PackedClause)
- type Weight = Integer
- data GCNF = GCNF {
- gcnfNumVars :: !Int
- gcnfNumClauses :: !Int
- gcnfLastGroupIndex :: !GroupIndex
- gcnfClauses :: [GClause]
- type GroupIndex = Int
- type GClause = (GroupIndex, PackedClause)
- data QDimacs = QDimacs {
- qdimacsNumVars :: !Int
- qdimacsNumClauses :: !Int
- qdimacsPrefix :: [QuantSet]
- qdimacsMatrix :: [PackedClause]
- data Quantifier
- type QuantSet = (Quantifier, [Atom])
- type Atom = Var
- type Lit = Int
- type Clause = [Lit]
- type PackedClause = Vector Lit
- packClause :: Clause -> PackedClause
- unpackClause :: PackedClause -> Clause
FileFormat class
module ToySolver.FileFormat.Base
CNF format
DIMACS CNF format
CNF | |
|
WCNF format
WCNF format for representing partial weighted Max-SAT problems.
This format is used for for MAX-SAT evaluations.
References:
WCNF | |
|
type WeightedClause = (Weight, PackedClause) Source #
Weighted clauses
GCNF format
Group oriented CNF Input Format
This format is used in Group oriented MUS track of the SAT Competition 2011.
References:
GCNF | |
|
type GroupIndex = Int Source #
Component number between 0 and gcnfLastGroupIndex
type GClause = (GroupIndex, PackedClause) Source #
Clause together with component number
QDIMACS format
QDIMACS format
Quantified boolean expression in prenex normal form,
consisting of a sequence of quantifiers (qdimacsPrefix
) and
a quantifier-free CNF part (qdimacsMatrix
).
References:
- QDIMACS standard Ver. 1.1 http://www.qbflib.org/qdimacs.html
QDimacs | |
|
data Quantifier Source #
Quantifier
Instances
type QuantSet = (Quantifier, [Atom]) Source #
Quantified set of variables
Re-exports
Positive (resp. negative) literals are represented as positive (resp. negative) integers. (DIMACS format).
type PackedClause = Vector Lit Source #
packClause :: Clause -> PackedClause Source #
unpackClause :: PackedClause -> Clause Source #