2

I would like to parse string with a propositional formula in CNF to DIMACS, thus a nested int list in haskell. The format is suitable for the haskell picosat bindings that seem to be more performant then other options for SAT solving.

The problem is that my code that implemented this is too complicated and now I am looking for a possible bug that is not obvious to find.

(My approach was to use the haskell hatt package, change the package so it uses Strings instead of single characters for variables names, parse the expression with hatt and then convert the resulting expression to the DIMACS format.)

I want to parse a string that represents a propositional formula in CNF notation (see example below). The result shoud be a nested list of ints. Thus the result should be suitable for solveAll that is part of the haskell picosat bindings.

Input:

-- "&" ... conjunction
-- "|" ... disjunction
-- "-" ... not operator

let myCNF = "GP  &  (-GP  |  Ma)  &  (-Ma  |  GP)  &  (-Ma  |  TestP)  &  (-Ma  |  Alg)  &  (-Ma  |  Src)  &  (-Ma  |  Hi)  &  (-Ma  |  Wg | X | Y) & -Z"

Result:

-- DIMACS format
-- every Variable (e.g., "GP") gets a number, say GP gets the int num 1
-- in case of not GP (i.e., "-GP") the int number representing the variable is negative, thus -1

-- Note: I hope I didn't do a type
let myresult = [[1], [-1, 2], [-2, 1], [-2, 3], [-2, 3], [-2, 5], [-2, 6], [-2, 7, 8, 9], [-10]]

let myvars = ["GP", "Ma", "TestP", "Alg", "Src", "Hi", "Wg", "X", "Y", "Z"]

-- or alternativly the variables are stored in an associative array
let varOtherWay = (1, GP), (2, Ma) (3, TestP), (4, Alg), (5, Src), (6, Hi), (7, Wg), (8, X), (9, Y), (10, Z)
4

2 回答 2

2

您可能不需要 parsec 来读取 CNF 中的语句，您可以提取变量map (splitOn "|") . splitOn "&"- 其余的只是将整数分配给变量：

import qualified Data.Map as M 
import Data.List.Split
import Control.Monad.State 

deleteMany c [] = []
deleteMany c (x:xs) 
  | x`elem`c  =     deleteMany c xs
  | otherwise = x : deleteMany c xs

parseStatement :: String -> ( [[Int]] , M.Map Int String )
parseStatement = 
 f . flip runState (M.empty, 1) . mapM (mapM (readVar . toVar)) . varsOf . deleteMany "() "
  where 
    f (r, (m, _)) = (r , M.fromList $ map (uncurry (flip (,))) $ M.toList m)

    varsOf = map (splitOn "|") . splitOn "&"

    toVar ('-':v) = (True , v)
    toVar v       = (False, v)

    readVar (b,v) = do 
      (m, c) <- get 
      case M.lookup v m of 
        Nothing -> put (M.insert v c m, c+1) >> return (neg b c)
        Just n  ->                              return (neg b n)

    neg True  = negate
    neg False = id

也许 parsec 版本对于错误处理或集成到更大的解析器中仍然很有趣：

parseStatement = parse statement "" . deleteMany " "

statement = sepBy1 clause (char '&')

clause = between (char '(') (char ')') x <|> x
  where x = sepBy1 var (char '|')

var = do
  n <- maybe False (const True) <$> optionMaybe (char '-')
  v <- many1 (noneOf "&|-() ")
  return (n, v)
于 2014-05-18T19:21:42.750 回答
0

我维护你提到的 picosat 绑定。看到这个问题后，我在picologicHackage 中添加了一个新包，它建立在picosat解析和转换命题公式的基础上，并将它们提供给 SAT 求解器。

import Picologic

p, q, r :: Expr
p = readExpr "~(A | B)"
q = readExpr "(A | ~B | C) & (B | D | E) & (D | F)"
r = readExpr "(φ <-> ψ)"

ps = ppExprU p
-- ¬(A ∨ B)
qs = ppExprU q
-- ((((A ∨ ¬B) ∨ C) ∧ ((B ∨ D) ∨ E)) ∧ (D ∨ F))
rs = ppExprU (cnf r)
-- ((φ ∧ (φ ∨ ¬ψ)) ∧ ((ψ ∨ ¬φ) ∧ ψ))

main :: IO ()
main = solveProp p >>= putStrLn . ppSolutions
-- ¬A ¬B
-- ¬A B
-- A ¬B

见：http ://hackage.haskell.org/package/picologic

于 2014-06-16T17:11:48.163 回答