保持“曲柄转动"的有效方法是:有状态的计算 [英] Efficient way to "keep turning the crank" on a stateful computation

问题描述

我有一个建模为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保持迭代该模型. /p>

所以这是我的问题:在这样的有状态计算中，我想将SMT变量作为输入输入到有状态计算中，有没有办法让SMT求解器转向它的曲柄以避免SBV的不良表现?

我想如果我有一个函数f :: St -> St和一个谓词p :: St -> SBool，而我想求解n :: SInt使得，假设Mergeable St，建议使用SBV进行此操作的建议方法是什么?

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

解决方案

完整的符号执行

如果没有看到我们可以执行的完整代码，很难理解. (当您发布人们可以实际运行的代码段时，堆栈溢出的效果最好.)但是，在程序中逐渐出现了一些指数复杂性的迹象.考虑一下您发布的以下细分:

         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构造必须评估"结构.每个步骤中的两个分支.并且您有一个嵌套的条件:这就是为什么您得到指数级减速的原因，每次迭代的系数为4.如您所见，这很快就变得不可用了. (考虑这种情况的一种方法是，SBV必须在每个步骤中运行那些嵌套if的所有可能结果.您可以绘制调用树以查看其呈指数增长.)

在不了解stepWorld或stepPlayer的详细信息的情况下，很难提出任何替代方案.但最重要的是，您希望尽可能消除对ite的那些调用，并将它们尽可能地推到递归链中.也许继续传递样式会有所帮助，但是这完全取决于这些操作的语义是什么，以及是否可以推迟"执行.决定成功.

查询模式

但是，我相信您可以尝试使用更好的方法是实际使用SBV的query模式.在这种模式下，您 not 不会在调用求解器之前先象征性地模拟所有内容.取而代之的是，您将约束逐步添加到求解器，查询可满足性，并根据获得的值采用不同的路径.我相信这种方法将在您的情况下最好地工作，在这种情况下，您可以动态地探索状态空间"状态.但也要一路做出决定.文档中有一个示例: 函数显示如何在增量模式(使用push/pop)中使用求解器一次浏览一次.

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

I have a stateful process that is modelled as an i -> RWS r w s a. I want to feed it an input cmds :: [i]; currently I do that wholesale:

    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

I can try searching for an input of a predetermined size like this:

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

However, this gives me horrible performance in SBV itself, i.e. before Z3 is called (I can see that this is the case because the verbose output shows me the all the time is spent before the (check-sat) call). This is even with inputLength set to something small like 4.

However, with inputLength set to 1 or 2, the whole process is very snappy. So this makes me hope that there is a way to run SBV to get the model of the behaviour of a single step i -> s -> (s, a), and then tell the SMT solver to keep iterating that model for n different is.

So that is my question: in a stateful computation like this, where I want to feed SMT variables as input into the stateful computation, is there a way to let the SMT solver turn its crank to avoid the bad performance of SBV?

I guess a simplified "model question" would be if I have a function f :: St -> St, and a predicate p :: St -> SBool, and I want to solve for n :: SInt such that p (iterateN n f x0), what is the recommended way of doing that with SBV, supposing Mergeable St?

EDIT: I've uploaded the whole code to Github but bear in mind it is not a minimalized example; in fact it isn't even very nice Haskell code yet.

解决方案

Full symbolic execution

It's hard to opine without seeing full code we can execute. (Stack-overflow works the best when you post code segments people can actually run.) But some of the tell-tale signs of exponential complexity is creeping in your program. Consider the following segment you posted:

        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

This looks like a "linear" walk if you are programming with concrete values. But keep in mind that the ite construct has to "evaluate" both branches in each step. And you have a nested if: This is why you're getting an exponential slow down, with a factor of 4 in each iteration. As you observed, this gets out-of-hand pretty quickly. (One way to think about this is that SBV has to run all possible outcomes of those nested-if's in each step. You can draw the call-tree to see this grows exponentially.)

Without knowing the details of your stepWorld or stepPlayer it's hard to suggest any alternative schemes. But bottom line, you want to eliminate those calls to ite as much as possible, and push them as low in the recursive chain as you possibly can. Perhaps continuation-passing style can help, but it all depends on what the semantics of these operations are, and if you can "defer" decisions successfully.

Query mode

However, I do believe that a better approach for you to try would be to actually use SBV's query mode. In this mode, you do not symbolically simulate everything first before calling the solver. Instead, you incrementally add constraints to the solver, query for satisfiability, and based on the values you get you take different paths. I believe this approach would work the best in your situation, where you dynamically explore the "state space" but also make decisions along the way. There is an example of this in the documentation: HexPuzzle. In particular, the search function shows how you can navigate one-move-at-a-time, using the solver in the incremental mode (using push/pop).

I'm not exactly sure if this model of execution matches the logic in your game. Hopefully, it can at least give you an idea. But I've had good luck with the incremental approach in the past where you can explore such large search-spaces incrementally by avoiding having to make all of the choices before you send things to z3.

这篇关于保持“曲柄转动"的有效方法是:有状态的计算的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！