如何使用 Haskell 快速生成 SBV 公式来处理数据？

Question

如何使用 Haskell 快速生成 SBV 公式来处理数据？

3

假设有一个树，其中节点可能存在也可能不存在，我想生成一个公式，其中：

对于每个节点都有一个布尔变量（表示它是否存在），
如果根节点没有被占用，则是自由的（可以存在也可以不存在），
当父节点存在时，子节点才能存在（子节点意味着父节点存在）。

我的目标是使用 allSat 生成给定形状的所有可能的子树。例如，考虑下面的数据类型和示例 tree：

data Tree
    = Leaf
    | Tree [ Tree ]
    deriving Show

tree :: Tree
tree
    = Tree            -- T1
        [ Leaf        -- L1
        , Tree        -- T2
            [ Leaf    -- L2
            , Leaf    -- L3
            ]
        ]

翻译该树应为每个节点引入布尔值T1，T2，L1，L2，L3以及一组约束条件：

L1 => T1
T2 => T1
L2 => T2
L3 => T2

以下代码生成正确的解决方案（11）：

main :: IO ()
main = do
    res <- allSat . forSome ["T1", "T2", "L1", "L2", "L3"] $
        \ (t1::SBool) t2 l1 l2 l3 ->
            (   (l1 ==> t1)
            &&& (t2 ==> t1)
            &&& (l2 ==> t2)
            &&& (l3 ==> t2)
            )
    putStrLn $ show res

那么，我如何生成给定某些具体的tree所给出的allSat方法的公式呢？

另一种解决方案是像这样构建操作：

main :: IO ()
main = do
    res <- allSat $ makePredicate tree
    putStrLn $ show res

makePredicate :: Tree -> Predicate
makePredicate    _     = do
        t1 <- exists "T1"
        l1 <- exists "L1"
        constrain $ l1 ==> t1
        t2 <- exists "T2"
        constrain $ t2 ==> t1
        l2 <- exists "L2"
        constrain $ l2 ==> t2
        l3 <- exists "L3"
        constrain $ l3 ==> t2
        return true

编辑：我发现了另一个与之相关的stackoverflow问题的答案。想法是在树的折叠过程中构建一个操作，就像上面的替代解决方案一样。这是可能的，因为Symbolic是一个单子。

- MichalAntkiew

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- MichalAntkiew · Accepted Answer

为了弄清楚递归该如何工作，有益的做法是重写问题中的替代解决方案以匹配树的形状：

makePredicate :: Tree -> Predicate
makePredicate    _     = do
        -- SBool for root
        t1 <- exists "T1"
        -- predicates for children
        c1 <- do
                -- SBool for child
                l1 <- exists "L1"
                -- child implies the parent
                constrain $ l1 ==> t1
                return true
        c2 <- do
                t2 <- exists "T2"
                constrain $ t2 ==> t1
                -- predicates for children
                c3 <- do
                        l2 <- exists "L2"
                        constrain $ l2 ==> t2
                        return true                    
                c4 <- do
                        l3 <- exists "L3"
                        constrain $ l3 ==> t2
                        return true
                return $ c3 &&& c4 &&& true 
        return $ c1 &&& c2 &&& true

正如我们所看到的，我们首先为节点创建一个SBool变量，然后处理它的子节点，最后返回一个合取范式。这意味着我们可以映射子节点以先生成它们的Predicate，然后将true作为初始值折叠Predicate列表。

下面的代码遍历树并生成公式。首先，我们简化Tree类型。

{-# LANGUAGE ScopedTypeVariables #-}
import Data.SBV

data Tree
    = Node String [ Tree ]
    deriving Show

tree :: Tree
tree
    = Node "T1"
        [ Node "L1" []
        , Node "T2"
            [ Node "L2" []
            , Node "L3" []
            ]
        ]

然后我们递归遍历树，并为每个节点生成一个Predicate。根节点是特殊的：因为它没有父节点，所以没有暗示。

main :: IO ()
main = do
    res <- allSat $ makeRootPredicate tree
    putStrLn $ show res

makeRootPredicate :: Tree       -> Predicate
makeRootPredicate    (Node i cs) = do
    x <- exists i
    cps <- mapM (makeNodePredicate x) cs
    return $ bAnd cps

makeNodePredicate :: SBool -> Tree       -> Predicate
makeNodePredicate    parent   (Node i cs) = do
    x <- exists i
    constrain $ x ==> parent
    cps <- mapM (makeNodePredicate x) cs
    return $ bAnd cps

最后，我正在使用bAnd来创建谓词的连词（正如评论中所指出的）。

由于bAnd在内部使用foldr，我们得到一个公式。

(c1 &&& (c2 &&& true))

替换c1和c2，我们得到：

(((l1 ==> t1) &&& true) &&& (((t2 ==> t1) &&& c3 &&& c4 &&& true) &&& true))

替换 c3 和 c4，我们得到

(((l1 ==> t1) &&& true) &&& (((t2 ==> t1) &&& ((l2 ==> t2) &&& true) &&& ((l3 ==> t2) &&& true) &&& true) &&& true))

正如评论中所指出的那样，SBV将在可能的情况下通过部分求值来内部简化公式。因此，true将被消除。