假设有一个树,其中节点可能存在也可能不存在,我想生成一个公式,其中:
以下代码生成正确的解决方案(11):
- 对于每个节点都有一个布尔变量(表示它是否存在),
- 如果根节点没有被占用,则是自由的(可以存在也可以不存在),
- 当父节点存在时,子节点才能存在(子节点意味着父节点存在)。
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是一个单子。
&&&
:你要找的是bAnd
函数:https://hackage.haskell.org/package/sbv-4.2/docs/src/Data-SBV-Utils-Boolean.html#bAndSBV 将通过部分求值内部"优化"这些嵌套调用,通常这样的布尔约束对底层 SMT 求解器的性能没有可见影响。 - aliasbAnd
。 - MichalAntkiew