ToySolver.Text.WCNF

Deprecated: Use ToySolver.FileFormat.CNF instead

Documentation

data WCNF

WCNF format for representing partial weighted Max-SAT problems.

This format is used for for MAX-SAT evaluations.

References:

• http://maxsat.ia.udl.cat/requirements/

Constructors

WCNF

Fields

• wcnfNumVars :: !Int

  Number of variables

• wcnfNumClauses :: !Int

  Number of (weighted) clauses

• wcnfTopCost :: !Weight

  Hard clauses have weight equal or greater than "top". We assure that "top" is a weight always greater than the sum of the weights of violated soft clauses in the solution.

• wcnfClauses :: [WeightedClause]

  Weighted clauses

Instances

Eq WCNF

Defined in ToySolver.FileFormat.CNF

Methods

(==) :: WCNF -> WCNF -> Bool

(/=) :: WCNF -> WCNF -> Bool

Ord WCNF

Defined in ToySolver.FileFormat.CNF

Methods

compare :: WCNF -> WCNF -> Ordering

(<) :: WCNF -> WCNF -> Bool

(<=) :: WCNF -> WCNF -> Bool

(>) :: WCNF -> WCNF -> Bool

(>=) :: WCNF -> WCNF -> Bool

max :: WCNF -> WCNF -> WCNF

min :: WCNF -> WCNF -> WCNF

Read WCNF

Defined in ToySolver.FileFormat.CNF

Methods

readsPrec :: Int -> ReadS WCNF

readList :: ReadS [WCNF]

readPrec :: ReadPrec WCNF

readListPrec :: ReadPrec [WCNF]

Show WCNF

Defined in ToySolver.FileFormat.CNF

Methods

showsPrec :: Int -> WCNF -> ShowS

show :: WCNF -> String

showList :: [WCNF] -> ShowS

FileFormat WCNF

Defined in ToySolver.FileFormat.CNF

Methods

parse :: ByteString -> Either String WCNF

render :: WCNF -> Builder

type WeightedClause = (Weight, PackedClause)

Weighted clauses

type Weight = Integer

Weigths must be greater than or equal to 1, and smaller than 2^63.

Parsing .cnf/.wcnf files

parseFile :: (FileFormat a, MonadIO m) => FilePath -> m (Either String a)

Parse a file but returns an error message when parsing fails.

parseByteString :: ByteString -> Either String WCNF

Parse a WCNF file but returns an error message when parsing fails.

Generating .wcnf files

writeFile :: (FileFormat a, MonadIO m) => FilePath -> a -> m ()

Write a value into a file.

hPutWCNF :: Handle -> WCNF -> IO ()

Output a WCNF to a Handle.

wcnfBuilder :: WCNF -> Builder

Encode a WCNF to a Builder