SATソルバーの実装に昨日あたり興味がわきまして、手始めにデータ構造とDIMACS CNFファイルのパーサーを書いて見ました。ファイルから読み込めるようになると今後開発するときのデバッグも用意になりますものね。
module Main where import System.Environment import Text.Parsec (char, oneOf, (<|>), many, many1, space, anyChar, manyTill, string, newline) import Text.Parsec.Prim (skipMany) import Text.Parsec.String (Parser, parseFromFile) natural :: Parser Int natural = do n <- oneOf ['1'..'9'] m <- many (oneOf ['0'..'9']) return (read (n : m)) type VarId = Int data Var = Var VarId deriving (Show, Eq) data Literal = Not Var | Normal Var deriving (Show, Eq) parseNotLiteral :: Parser Literal parseNotLiteral = do { char '-'; n <- natural; return (Not (Var n)); } parseNormalLiteral :: Parser Literal parseNormalLiteral = do { n <- natural; return (Normal (Var n)); } parseLiteral :: Parser Literal parseLiteral = parseNotLiteral <|> parseNormalLiteral data Clause = EmptyClause | Clause [Literal] | UnitClause Literal deriving (Show, Eq) parseEOL :: Parser Char parseEOL = do { space; char '0'; } parseLiterals :: Parser [Literal] parseLiterals = do { l <- parseLiteral; space; ls <- parseLiterals; return (l:ls); } <|> do { char '0'; return []; } parseClause :: Parser Clause parseClause = do { ls <-parseLiterals; newline; case (length ls) of 0 -> return EmptyClause 1 -> return $ UnitClause (head ls) _ -> return $ Clause ls } data CNF = CNF [Clause] deriving (Show) parseCNF :: Parser CNF parseCNF = do { cs <- many1 parseClause; return (CNF cs); } parseComment :: Parser String parseComment = do { char 'c'; space; comment <- (manyTill anyChar newline); return comment } type VariableCount = Int type ClauseCount = Int data Header = Header VariableCount ClauseCount deriving (Show) parseHeader :: Parser Header parseHeader = do { char 'p'; space; string "cnf"; space; vc <- natural; space; cc <- natural; newline; return (Header vc cc); } data DIMACS = DIMACS { _variableCount :: VariableCount ,_clauseCount :: ClauseCount ,_cnf :: CNF } deriving (Show) parseDIMACS = do { skipMany parseComment; header <- parseHeader; cnf <- parseCNF; return cnf; case header of (Header vc cc) -> return DIMACS { _variableCount = vc ,_clauseCount = cc ,_cnf = cnf}; } main :: IO () main = do { args <- getArgs; dimacs <- parseFromFile parseDIMACS (args !! 0); case dimacs of Left err -> print err Right xs -> print xs }
parsec3は何度やってもなれませんね、もっとApplicativeスタイルでかけるといいんですが。
とりあえず、以下のような
c This is a test cnf file. c This is a comment line. p cnf 3 2 1 2 3 0 -2 3 0
ようなファイルを与えると、
DIMACS {_variableCount = 3, _clauseCount = 2, _cnf = CNF [Clause [Normal (Var 1),Normal (Var 2),Normal (Var 3)],Clause [Not (Var 2),Normal (Var 3)]]}
と帰ってきます。