haskell - SAT 解决与 haskell SBV 库 : how to generate a predicate from a parsed string?

Question

我想解析 String它描述了一个命题公式，然后使用 SAT 求解器找到该命题公式的所有模型。

现在我可以用 hatt 解析一个命题公式包裹;见testParse下面的功能。

我还可以使用 SBV 库运行 SAT 求解器调用；见testParse下面的功能。

问题:
如何在运行时生成 Predicate 类型的值喜欢 myPredicate在 SBV 库中表示我刚刚从字符串解析的命题公式？我只知道如何手动输入 forSome_ $ \x y z -> ...表达式，但不是如何从 Expr 编写转换器函数值转换为 Predicate 类型的值.

-- cabal install sbv hatt
import Data.Logic.Propositional
import Data.SBV


-- Random test formula:
-- (x or ~z) and (y or ~z)

-- graphical depiction, see: https://www.wolframalpha.com/input/?i=%28x+or+~z%29+and+%28y+or+~z%29

testParse = parseExpr "test source" "((X | ~Z) & (Y | ~Z))"

myPredicate :: Predicate
myPredicate = forSome_ $ \x y z -> ((x :: SBool) ||| (bnot z)) &&& (y ||| (bnot z))

testSat = do 
         x <- allSat $ myPredicate
         putStrLn $ show x     


main = do
       putStrLn $ show $ testParse
       testSat


    {-
       Need a function that dynamically creates a Predicate 
(as I did with the function (like "\x y z -> ..") for an arbitrary expression of type "Expr" that is parsed from String. 
    -}

可能有用的信息:

这是 BitVectors.Data 的链接:
http://hackage.haskell.org/package/sbv-3.0/docs/src/Data-SBV-BitVectors-Data.html

这是示例代码形式 Examples.Puzzles.PowerSet:

import Data.SBV

genPowerSet :: [SBool] -> SBool
genPowerSet = bAll isBool
  where isBool x = x .== true ||| x .== false

powerSet :: [Word8] -> IO ()
powerSet xs = do putStrLn $ "Finding all subsets of " ++ show xs
                 res <- allSat $ genPowerSet `fmap` mkExistVars n

这是 Expr 数据类型(来自 hatt 库):

data Expr = Variable      Var
          | Negation      Expr
          | Conjunction   Expr Expr
          | Disjunction   Expr Expr
          | Conditional   Expr Expr
          | Biconditional Expr Expr
          deriving Eq

Answer 1

与 SBV 合作

使用 SBV 要求您遵循类型并实现 Predicate只是一个 Symbolic SBool .在这一步之后，调查和发现 Symbolic 很重要。是一个单子(monad) - 是的，一个单子(monad)!

既然你知道你有一个单子(monad)，那么黑线鳕中的任何东西都是Symbolic结合起来构建您想要的任何 SAT 应该是微不足道的。对于您的问题，您只需要在 AST 上构建一个简单的解释器即可构建 Predicate .

代码演练

代码全部包含在下面的一个连续形式中，但我将逐步介绍有趣的部分。入口点是solveExpr它接受表达式并产生一个 SAT 结果:

solveExpr :: Expr -> IO AllSatResult
solveExpr e0 = allSat prd

SBV的应用 allSat谓词是显而易见的。要构建该谓词，我们需要声明一个存在的 SBool对于我们表达式中的每个变量。现在让我们假设我们有 vs :: [String]其中每个字符串对应于 Var 之一从表达式。

  prd :: Predicate
  prd = do
      syms <- mapM exists vs
      let env = M.fromList (zip vs syms)
      interpret env e0

请注意编程语言基础知识是如何潜入这里的。我们现在需要一个将表达式变量名称映射到 SBV 使用的符号 bool 值的环境。

接下来我们解释表达式以产生我们的 Predicate .解释函数使用环境并仅应用与 hatt 的 Expr 中的每个构造函数的意图相匹配的 SBV 函数。类型。

  interpret :: Env -> Expr -> Predicate
  interpret env expr = do
   let interp = interpret env
   case expr of
    Variable v -> return (envLookup v env)
    Negation e -> bnot `fmap` interp e
    Conjunction e1 e2   ->
     do r1 <- interp e1
        r2 <- interp e2
        return (r1 &&& r2)
    Disjunction e1 e2   ->
     do r1 <- interp e1
        r2 <- interp e2
        return (r1 ||| r2)
    Conditional e1 e2   -> error "And so on"
    Biconditional e1 e2 -> error "And so on"

就是这样!其余的只是样板。

完整代码

import Data.Logic.Propositional hiding (interpret)
import Data.SBV
import Text.Parsec.Error (ParseError)
import qualified Data.Map as M
import qualified Data.Set as Set
import Data.Foldable (foldMap)
import Control.Monad ((<=<))

testParse :: Either ParseError Expr
testParse = parseExpr "test source" "((X | ~Z) & (Y | ~Z))"

type Env = M.Map String SBool

envLookup :: Var -> Env -> SBool
envLookup (Var v) e = maybe (error $ "Var not found: " ++ show v) id
                            (M.lookup [v] e)

solveExpr :: Expr -> IO AllSatResult
solveExpr e0 = allSat go
 where
  vs :: [String]
  vs = map (\(Var c) -> [c]) (variables e0)

  go :: Predicate
  go = do
      syms <- mapM exists vs
      let env = M.fromList (zip vs syms)
      interpret env e0
  interpret :: Env -> Expr -> Predicate
  interpret env expr = do
   let interp = interpret env
   case expr of
    Variable v -> return (envLookup v env)
    Negation e -> bnot `fmap` interp e
    Conjunction e1 e2   ->
     do r1 <- interp e1
        r2 <- interp e2
        return (r1 &&& r2)
    Disjunction e1 e2   ->
     do r1 <- interp e1
        r2 <- interp e2
        return (r1 ||| r2)
    Conditional e1 e2   -> error "And so on"
    Biconditional e1 e2 -> error "And so on"

main :: IO ()
main = do
       let expr = testParse
       putStrLn $ "Solving expr: " ++ show expr
       either (error . show) (print <=< solveExpr) expr