SAT使用haskell SBV库解决问题：如何从解析的字符串生成谓词？ [英] SAT solving with haskell SBV library: how to generate a predicate from a parsed string?

问题描述

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

现在我可以使用 hatt 包解析命题公式;请参阅下面的 testParse 函数。

我也可以使用SBV库运行SAT解算器调用;请参阅下面的 testParse 函数。

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

   -  cabal install sbv hatt 
导入Data.Logic.Propositional 
导入Data.SBV 
 
 
  - 随机测试公式：
  - （x或〜z）和（y或〜z）
 
 - 图形描述，请参阅：https://www.wolframalpha.com/input/?i=%28x+or+~z%29+and+%28y+or+~z%29 
 
 testParse = parseExprtest source（（X |〜Z）&（Y |〜Z））
 
 myPredicate :: Predicate 
 myPredicate = forSome_ $ \xyz  - > （（x :: SBool）|||（bnot z））&&& （y |||（bnot z））
 
 testSat = do 
x<  -  allSat $ myPredicate 
 putStrLn $ show x 
 
 
 main = do 
 putStrLn $ show $ testParse 
 testSat 
 
 
 { -  
需要一个动态创建Predicate 
（as对于从String解析的Expr类型的任意表达式，我使用了函数（如\xyz-> ..）。
  - } 
  
 
 
可能有帮助的信息： 
 
 
以下是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 
其中isBool x = x。== true ||| x。== false 
 
 powerSet :: [Word8]  - > IO（）
 powerSet xs = do putStrLn $查找++ show xs 
 res的所有子集 -  allSat $ genPowerSet`fmap` mkExistVars n 
  
以下是Expr数据类型（来自hatt库）： 
 
 
  data Expr =变量
 |否定前期
 |连接Expr Expr 
 | Disjunction Expr Expr 
 | Conditional Expr Expr 
 | Biconditional Expr Expr 
派生方程
  
 
 
解决方案
 使用SBV  
 
 
 
使用SBV需要您遵循这些类型并实现 Predicate 为只是一个符号SBool 。在这一步之后，重要的是你要调查和发现符号是一个monad  -  yay，一个monad！ 
 
 
现在你知道你有一个monad，那么黑道中任何小于符号的任何东西都应该是微不足道的，以便构建任何你想要的SAT。对于你的问题，你只需要一个简单的解释器来建立一个 Predicate 。
 
 
 
  - 通过 
 
 
 
代码全部包含在下面的一个连续表单中，但我将逐步浏览有趣的部分。入口点是 solveExpr ，它需要表达式并产生SAT结果： 
 
 
  solveExpr :: Expr  - > IO AllSatResult 
 solveExpr e0 = allSat prd 
  
 SBV的应用 allSat 到谓词很明显。为了构建谓词，我们需要为表达式中的每个变量声明一个存在> SBool 。现在让我们假设我们有 vs :: [String] ，其中每个字符串都与表达式中的 Var 之一相对应。
 
 
  prd :: Predicate 
 prd = do 
 syms<  -  mapM存在vs 
 let env = M.fromList（zip vs syms）
 interpret env e0 
  
注意编程语言的基础就是在这里偷偷摸摸的。我们现在需要一个将表达式变量名称映射到SBV使用的符号布尔值的环境。
接下来我们解释表达式来产生我们的 Predicate 。解释函数使用环境，并且只应用匹配来自hatt的 Expr 类型的每个构造函数的意图的SBV函数。
  interpret :: Env  - > Expr  - >谓词
解释env expr = do 
 let interp =解释env 
 
的变量expr $变量v  - >返回（envLookup v env）
否定e  - > bnot`fmap` interp e 
连接e1 e2  - > 
 do r1 < -  interp e1 
 r2 < -  interp e2 
 return（r1&& r2）
分离e1 e2  - > 
 do r1 < -  interp e1 
 r2 < -  interp e2 
 return（r1 ||| r2）
条件e1 e2  - >错误等等
 Biconditional e1 e2  - >错误等等
  
就是这样！ 
 
 
 完整代码 
 导入Data.Logic.Propositional隐藏（解释）
导入Data.SBV 
导入Text.Parsec.Error（ParseError）
将限定的Data.Map导入为M 
 import qualified Data.Set as Set 
 import Data.Foldable（foldMap）
 import Control.Monad（（<< =））
 
 testParse :: ParseError Expr 
 testParse = parseExprtest source（（X |〜Z）&（Y |〜Z））
 
类型Env = M.Map字符串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 
其中
 vs :: [String] 
 vs = map（\（Var c） - > [c]）（variables e0 ）
 $ b $ go ::谓词
 go = do 
 syms<  -  mapM exists vs 
 let env = M.fromList（zip vs syms）
 interpret env e0 
 interpret :: Env  - > Expr  - >谓词
解释env expr = do 
 let interp =解释env 
 
的变量expr $变量v  - >返回（envLookup v env）
否定e  - > bnot`fmap` interp e 
连接e1 e2  - > 
 do r1 < -  interp e1 
 r2 < -  interp e2 
 return（r1&& r2）
分离e1 e2  - > 
 do r1 < -  interp e1 
 r2 < -  interp e2 
 return（r1 ||| r2）
条件e1 e2  - >错误等等
 Biconditional e1 e2  - >错误等
 $ b $ main main :: IO（）
 main = do 
 let expr = testParse 
 putStrLn $解决expr：++ show expr 
（error。show）（print <=< solveExpr）expr 
  
 
I want to parse a String that depicts a propositional formula and then find all models of the propositional formula with a SAT solver.

Now I can parse a propositional formula with the hatt package; see the testParse function below.

I can also run a SAT solver call with the SBV library; see the testParse function below.

Question:
How do I, at runtime, generate a value of type Predicate like myPredicate within the SBV library that represents the propositional formula I just parsed from a String? I only know how to manually type the forSome_ $ \x y z -> ... expression, but not how to write a converter function from an Expr value to a value of type 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. 
    -}
Information that might be helpful:

Here is the link to the BitVectors.Data:
http://hackage.haskell.org/package/sbv-3.0/docs/src/Data-SBV-BitVectors-Data.html

Here is example code form 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
Here is the Expr data type (from hatt library):
data Expr = Variable      Var
          | Negation      Expr
          | Conjunction   Expr Expr
          | Disjunction   Expr Expr
          | Conditional   Expr Expr
          | Biconditional Expr Expr
          deriving Eq

解决方案
Working With SBV

Working with SBV requires that you follow the types and realize the Predicate is just a Symbolic SBool.  After that step it is important that you investigate and discover Symbolic is a monad - yay, a monad!

Now that you you know you have a monad then anything in the haddock that is Symbolic should be trivial to combine to build any SAT you desire.  For your problem you just need a simple interpreter over your AST that builds a Predicate.

Code Walk-Through

The code is all included in one continuous form below but I will step through the fun parts. The entry point is solveExpr which takes expressions and produces a SAT result:
solveExpr :: Expr -> IO AllSatResult
solveExpr e0 = allSat prd
The application of SBV's allSat to the predicate is sort of obvious.  To build that predicate we need to declare an existential SBool for every variable in our expression.  For now lets assume we have vs :: [String] where each string corresponds to one of the Var from the expression.
  prd :: Predicate
  prd = do
      syms <- mapM exists vs
      let env = M.fromList (zip vs syms)
      interpret env e0
Notice how programming language fundamentals is sneaking in here.  We now need an environment that maps the expressions variable names to the symbolic booleans used by SBV.

Next we interpret the expression to produce our Predicate.   The interpret function uses the environment and just applies the SBV function that matches the intent of each constructor from hatt's Expr type.
  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"
And that is it!  The rest is just boiler-plate.

Complete Code
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


                        
这篇关于SAT使用haskell SBV库解决问题：如何从解析的字符串生成谓词？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！