13

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

现在我可以用hatt包解析命题公式了；请参阅testParse下面的功能。

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

问题： 在运行时，我如何在 SBV 库中生成一个类型的值，该值Predicate表示myPredicate我刚刚从字符串中解析的命题公式？我只知道如何手动键入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
4

2 回答 2

10

与 SBV 合作

使用 SBV 要求您遵循类型并意识到Predicate它只是一个Symbolic SBool. 在这一步之后，重要的是你调查并发现Symbolic它是一个单子——是的，一个单子！

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

代码演练

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

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

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

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

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

接下来我们解释表达式以产生我们的Predicate. 解释函数使用环境并仅应用与 hattExpr类型中每个构造函数的意图相匹配的 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
于 2014-04-23T04:44:17.653 回答
4

forSome_是Provable该类的成员，因此定义 instance 似乎就足够了Provable Expr。几乎所有功能都在SVB使用中Provable，因此您可以在本地使用所有这些功能Expr。首先，我们将 a 转换为Expr在 a 中查找变量值的函数Vector。您也可以使用Data.Map.Map或类似的东西，但环境一旦创建就不会改变并Vector提供恒定的时间查找：

import Data.Logic.Propositional
import Data.SBV.Bridge.CVC4
import qualified Data.Vector as V
import Control.Monad

toFunc :: Boolean a => Expr -> V.Vector a -> a
toFunc (Variable (Var x)) = \env -> env V.! (fromEnum x)
toFunc (Negation x) = \env -> bnot (toFunc x env)
toFunc (Conjunction a b) = \env -> toFunc a env &&& toFunc b env
toFunc (Disjunction a b) = \env -> toFunc a env ||| toFunc b env
toFunc (Conditional a b) = \env -> toFunc a env ==> toFunc b env
toFunc (Biconditional a b) = \env -> toFunc a env <=> toFunc b env

Provable本质上定义了两个函数：forAll_, forAll, forSome_, forSome. 我们必须生成所有可能的变量到值的映射并将函数应用于映射。选择如何准确处理结果将由Symbolicmonad 完成：

forAllExp_ :: Expr -> Symbolic SBool
forAllExp_ e = (m0 >>= f . V.accum (const id) (V.replicate (fromEnum maxV + 1) false)
  where f = return . toFunc e 
        maxV = maximum $ map (\(Var x) -> x) (variables e)
        m0 = mapM fresh (variables e)

wherefresh是一个函数，它通过将给定变量与所有可能的值相关联来“量化”给定变量。

fresh :: Var -> Symbolic (Int, SBool)
fresh (Var var) = forall >>= \a -> return (fromEnum var, a)

如果您为这四个函数中的每一个定义其中一个函数，您将拥有大量非常重复的代码。因此，您可以将上述概括如下：

quantExp :: (String -> Symbolic SBool) -> Symbolic SBool -> [String] -> Expr -> Symbolic SBool
quantExp q q_ s e = m0 >>= f . V.accum (const id) (V.replicate (fromEnum maxV + 1) false)
  where f = return . toFunc e 
        maxV = maximum $ map (\(Var x) -> x) (variables e)
        (v0, v1) = splitAt (length s) (variables e)
        m0 = zipWithM fresh (map q s) v0 >>= \r0 -> mapM (fresh q_) v1 >>= \r1 -> return (r0++r1)

fresh :: Symbolic SBool -> Var -> Symbolic (Int, SBool)
fresh q (Var var) = q >>= \a -> return (fromEnum var, a)

如果确切地混淆了正在发生的事情，则该Provable实例可能足以解释：

instance Provable Expr where 
  forAll_  = quantExp forall forall_ [] 
  forAll   = quantExp forall forall_ 
  forSome_ = quantExp exists exists_ []
  forSome  = quantExp exists exists_

然后你的测试用例：

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

myPredicate' :: Predicate
myPredicate' = forSome_ $ let Right a = parseExpr "test source" "((X | ~Z) & (Y | ~Z))" in a

testSat = allSat myPredicate >>= print
testSat' = allSat myPredicate >>= print
于 2014-04-23T05:13:55.057 回答