DIMACS CNFパーサーを書いた。

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)]]}

と帰ってきます。