Разобрать строку с пропозициональной формулой в CNF в список вложенных целых чисел DIMACS в haskell

Я хотел бы проанализировать строку с пропозициональной формулой в CNF для DIMACS, таким образом, вложенный список int в haskell. Формат подходит для привязок haskell picosat, которые кажутся более производительными, чем другие варианты решения SAT.

Проблема в том, что мой код, который реализовал это, слишком сложен, и теперь я ищу возможную ошибку, которую невозможно найти.

(Мой подход состоял в том, чтобы использовать пакет haskell hatt, изменить пакет, чтобы он использовал строки вместо отдельных символов для имен переменных, проанализировать выражение с помощью hatt, а затем преобразовать полученное выражение в формат DIMACS.)

Я хочу разобрать строку, представляющую пропозициональную формулу в нотации CNF (см. пример ниже). Результатом должен быть вложенный список целых чисел. Таким образом, результат должен подходить для solveAll, являющегося частью haskell picosat. привязки.

Вход:

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

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

Результат:

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

haskell satisfiability
person mrsteve    schedule 18.05.2014    source источник
comment
Так где твоя попытка?   -  person Sean Perry    schedule 18.05.2014
comment
Я использовал очень сложный маршрут, скопировал и вставил исходный пакет шляпы с github.com/beastaugh/hatt. и адаптировал его. Но я не использовал git, поэтому могу даже вставить сюда git diff. Я не уверен, что размещение zip-файла где-то помогает. Если бы я сделал это снова, я бы, возможно, просто разделил строку. Однако у меня есть ощущение, что это можно сделать в 3-4 строки с помощью parsec, но я еще недостаточно знаком, чтобы использовать его так, как я доверяю своему коду. Мне еще многое предстоит узнать о Haskell.   -  person mrsteve    schedule 18.05.2014

Ответы (2)


arrow_upward
2
arrow_downward

Вам, вероятно, не нужен парсек для чтения инструкций в 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)
person user2407038    schedule 18.05.2014

arrow_upward
0
arrow_downward

Я поддерживаю привязки к пикосату, о которых вы упомянули. Увидев этот вопрос, я добавил в Hackage новый пакет picologic, который основан на 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

person Stephen Diehl    schedule 16.06.2014