使用haskell SBV库解决SAT:如何从解析后的字符串生成谓词？

Question

我想解析一个String描述命题公式,然后用SAT求解器找到命题公式的所有模型.

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

我也可以用SBV库运行SAT求解器调用; 看testParse下面的功能.

问题: 如何在运行时生成Predicate类似于myPredicateSBV库中的类型值,该值表示我刚从String中解析的命题公式？我只知道如何手动键入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 BEI.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 - yay,a 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使用的符号布尔值.

接下来我们解释表达式来生成我们的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