2

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.

1 Answer 1

2

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.

7
  • I've uploaded the full code to Github; see the link edited into the question.
    – Cactus
    Commented Jul 4, 2020 at 3:06
  • So, my whole goal was to see if I can use SBV with an interpreter that is deliberately written in a straightforward style -- basically, write it using concrete values, then change the state coordinates to be symbolic, and then go. If I understand your first point here, this approach is wholly infeasable.
    – Cactus
    Commented Jul 4, 2020 at 3:07
  • 1
    Expecting a straightforward coding of the interpreter to work well symbolically isn't realistic, as you found out. This is the classic state-space explosion problem, and is a major obstacle in symbolic simulation systems.
    – alias
    Commented Jul 6, 2020 at 17:40
  • 1
    I'm not too familiar with Rossette, but I'd be surprised if they can run symbolic programs as fast as concrete ones. Even if you can symbolically execute fast, the SAT/SMT solver will take its time: You're essentially turning "check if this is a satisfying instance" (a polynomial time algorithm) to "find a satisfying instance" (which is NP-complete.) Perhaps Rossette uses smarter heuristics in the front-end, but the fundamental complexity remains. I'd love to see references that show otherwise.
    – alias
    Commented Jul 8, 2020 at 1:52
  • 1
    That is true. But symbolic simulation has similar costs that stem from similar reasons. Whenever there's an if-then-else, you have to "execute" both branches and merge the results. When you model array-access, you cannot do a "simple" lookup: You have to scan the entire array for the symbolic address match. These typically do add up to significant work before you even start "solving." A rough comparison is that you have to unroll every possible execution path, and put mux'es at the end of each of those to merge the results. Doing that efficiently is an art form, as much as engineering.
    – alias
    Commented Jul 8, 2020 at 14:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.