Эффективный способ "продолжать крутить ручку" при вычислении с отслеживанием состояния

Question

У меня есть процесс с отслеживанием состояния, который смоделирован как 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с.

Итак, вот мой вопрос: в таких вычислениях с сохранением состояния, где я хочу передать переменные SMT в качестве входных данных для вычислений с сохранением состояния, есть ли способ позволить решателю SMT повернуть рукоятку, чтобы избежать плохой работы SBV?

Я предполагаю, что упрощенный "модельный вопрос" будет, если у меня есть функцияf :: St -> St, и предикат p :: St -> SBool, и я хочу решить n :: SInt такой, что p (iterateN n f x0), каков рекомендуемый способ сделать это с SBV, предполагая Mergeable St?

РЕДАКТИРОВАТЬ: я загрузил весь код в Github, но имейте в виду, что это не минимизированный пример; на самом деле это даже не очень хороший код на Haskell.

Answer 1

Полное символическое исполнение

Трудно высказывать мнение, не видя полного кода, который мы можем выполнить. (Переполнение стека работает лучше всего, когда вы публикуете сегменты кода, которые люди действительно могут запустить.) Но некоторые из контрольных признаков экспоненциальной сложности проявляются в вашей программе. Рассмотрим следующий сегмент, который вы разместили:

        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

Это выглядит как "линейный" ход, если вы программируете с конкретными значениями. Но имейте в виду, чтоiteconstruct должен "оценивать" обе ветви на каждом шаге. И у вас есть вложенное if: вот почему вы получаете экспоненциальное замедление с коэффициентом 4 на каждой итерации. Как вы заметили, это довольно быстро выходит из-под контроля. (Один из способов подумать об этом состоит в том, что SBV должен запускать все возможные результаты этих вложенных if на каждом шаге. Вы можете нарисовать дерево вызовов, чтобы увидеть, как оно растет экспоненциально.)

Не зная подробностей вашего stepWorld или stepPlayerАльтернативные схемы предложить сложно. Но суть в том, что вы хотите устранить эти призывы кiteкак можно больше и продвигайте их как можно ниже в рекурсивной цепочке. Возможно, поможет стиль передачи продолжения, но все зависит от семантики этих операций и от того, можете ли вы успешно "отложить" решения.

Режим запроса

Тем не менее, я считаю, что лучший подход для вас - это использовать SBV. queryРежим. В этом режиме вы не симулируете все сначала перед вызовом решателя. Вместо этого вы постепенно добавляете ограничения к решающей программе, запрашиваете выполнимость и в зависимости от полученных значений выбираете разные пути. Я считаю, что этот подход будет лучше всего работать в вашей ситуации, когда вы динамически исследуете "пространство состояний", но также принимаете решения на этом пути. В документации есть пример: HexPuzzle. В частности, search показывает, как можно перемещаться по одному за раз, используя решающую программу в инкрементальном режиме (используя push/pop).

Я не совсем уверен, соответствует ли эта модель исполнения логике вашей игры. Надеюсь, это может хотя бы дать вам представление. Но в прошлом мне повезло с инкрементным подходом, когда вы могли постепенно исследовать такие большие поисковые пространства, избегая необходимости делать все варианты перед отправкой данных на z3.