2

我有一个建模为i -> RWS r w s a. 我想给它一个输入cmds :: [i]；目前我做批发：

    let play = runGame theGame . go
          where
            go [] = finished
            go ((v, n):cmds) = do
                end1 <- stepWorld
                end2 <- ite (SBV.isJust end1) (return end1) $ stepPlayer (v, n)
                ite (SBV.isJust end2) (return end2) $ go cmds

我可以尝试搜索预定大小的输入，如下所示：

    result <- satWith z3{ verbose = True } $ do
        cmds <- mapM sCmd [1..inputLength]
        return $ SBV.fromMaybe sFalse $ fst $ play cmds

但是，这给了我在 SBV 本身中的可怕性能，即在调用 Z3 之前（我可以看到情况就是这样，因为verbose输出显示我在调用之前花费的所有时间(check-sat)）。即使inputLength设置为像 4 这样的小值也是如此。

但是，inputLength设置为 1 或 2 时，整个过程非常快速。所以这让我希望有一种方法可以运行 SBV 来获得单步行为的模型i -> s -> (s, a)，然后告诉 SMT 求解器继续针对n不同i的 s 迭代该模型。

所以这是我的问题：在这样的有状态计算中，我想将SMT 变量作为输入提供给有状态计算，有没有办法让 SMT 求解器转动曲柄以避免 SBV 的不良性能？

我想一个简化的“模型问题”是如果我有一个函数f :: St -> St和一个谓词p :: St -> SBool，我想解决n :: SInt这样p (iterateN n f x0)的问题，假设用 SBV 做这件事的推荐方法是什么Mergeable St？

编辑：我已将整个代码上传到 Github，但请记住这不是一个最小化的示例；事实上，它甚至还不是很好的 Haskell 代码。

4

1 回答 1

2

完全符号执行

如果没有看到我们可以执行的完整代码，就很难发表意见。（当您发布人们可以实际运行的代码段时，Stack-overflow 效果最好。）但是指数复杂性的一些明显迹象正在您的程序中蔓延。考虑您发布的以下部分：

        go [] = finished
        go ((v, n):cmds) = do
                end1 <- stepWorld
                end2 <- ite (SBV.isJust end1) (return end1) $ stepPlayer (v, n)
                ite (SBV.isJust end2) (return end2) $ go cmds

如果您使用具体值进行编程，这看起来像是“线性”步行。但请记住，ite构造必须在每个步骤中“评估”两个分支。而且您有一个嵌套的 if：这就是为什么您会以指数方式减速的原因，每次迭代中的因子为 4。正如您所观察到的，这很快就会失控。（考虑这一点的一种方法是，SBV 必须在每一步中运行这些嵌套 if 的所有可能结果。您可以绘制调用树以查看它呈指数增长。）

在不知道您的详细信息的情况下，stepWorld或者stepPlayer很难提出任何替代方案。但归根结底，您希望ite尽可能多地消除这些调用，并尽可能将它们推到递归链的最低位置。也许延续传递风格会有所帮助，但这完全取决于这些操作的语义是什么，以及您是否可以成功“推迟”决策。

查询方式

但是，我确实相信您尝试的更好方法是实际使用 SBVquery模式。在这种模式下，您不会在调用求解器之前先象征性地模拟所有内容。相反，您逐渐向求解器添加约束，查询可满足性，并根据您获得的值采取不同的路径。我相信这种方法最适合您的情况，您可以动态地探索“状态空间”，但也可以在此过程中做出决策。文档中有一个例子：HexPuzzle。特别是，该search函数显示了如何在增量模式下使用求解器（使用push/ pop）一次导航一个动作。

我不确定这种执行模型是否符合您游戏中的逻辑。希望它至少可以给你一个想法。但是我过去对增量方法很幸运，您可以通过避免在将内容发送到 z3 之前做出所有选择来逐步探索如此大的搜索空间。

于 2020-07-03T14:47:38.370 回答