Почему сортировка Int32 намного медленнее, чем сортировка Integer в этом коде SBV/Z3?

Question

Пытаясь изучить Z3, я попытался решить одну из моих любимых задач, связанных с появлением кода (особенно сложную, 2018 день 23, часть 2), с помощью привязок Haskell.sbv. Впереди спойлеры в коде...

module Lib
    ( solve
    ) where

import Data.SBV

puzzle :: [((SInteger, SInteger, SInteger), SInteger)]
puzzle = (\((x, y, z), r) -> ((literal x, literal y, literal z), literal r)) <$> [
      ((60118729,58965711,8716524), 71245377),
      {- 999 more values that are large like the first one... -}
]

manhattan (a1, a2, a3) (b1, b2, b3) =
  abs (a1 - b1) + abs (a2 - b2) + abs (a3 - b3)

countInRange pos =
  foldr (\(nb, r) -> (+) $ oneIf (manhattan nb pos .<= r)) (0 :: SInteger) puzzle

answer = optimize Lexicographic $ do
  x <- sInteger "x"
  y <- sInteger "y"
  z <- sInteger "z"
  maximize "in-range"             $ countInRange (x, y, z)
  minimize "distance-from-origin" $ abs x + abs y + abs z

solve =
  answer >>= print

Теперь этот вопрос не совсем sbv вопрос, ни вопрос Haskell, и в приведенном выше коде нет ничего плохого (он решает 1000 значений -puzzleсписки с огромными координатами X,Y и Z чуть более чем за минуту на моей машине, что для меня достаточно). Этот вопрос о(0 :: SInteger) найти в countInRange.

Если я изменю (0 :: SInteger) к (0 :: SInt32) это приводит к тому, что решение занимает очень-очень много времени (я запустил его, когда начал вводить этот вопрос, а это было 16 минут назад и продолжает подсчет).

Итак, что дает? ПочемуSInt32в этом случае намного медленнее? Это потому, что я смешиваю домены (используяSIntegerв другом месте)? Я бы подумал, что безграничныйSInteger представление будет медленнее, чем ограниченное Int32.

Обратите внимание, что рассматриваемый символический тип используется только для подсчета совпадающих значений из puzzle (таким образом, он всегда будет <= 1000, т.е. длина puzzle).

ОБНОВЛЕНИЕ Я убилInt32 раствор через 40 минут работы.

Answer 1

Когда вы кодируете подобную проблему в SBV, есть два места, где может сыграть роль производительность:

• SBV может потребоваться много времени для создания самого запроса
• SBV отправляет запрос в решающую программу, но решающая программа долго не отвечает

Судя по вашему описанию, это последнее; но вы можете убедиться в этом, позвонивoptimize нравится:

optimizeWith z3{verbose=True} ...

Что это будет делать, так это распечатать взаимодействие SBV с серверным решателем. В какой-то момент вы увидите:

[SEND] (check-sat)

Это означает, что SBV выполнила свою работу и теперь ждет, пока решатель вернется с ответом. Снова запустите вашу программу с включенной опцией. Если SBV не торопится, вы не увидите вышеупомянутого[SEND] (check-sat)линия, и об этом следует сообщить здесь как о проблеме SBV: https://github.com/LeventErkok/sbv/issues

Однако более вероятно, что SBV отправляет check-sat нормально, но решающая программа намного дольше реагирует, когда вы используете SInt32 в отличие от SInteger.

Если предположить, что это так, то это, вероятно, связано с тем, что вашу проблему намного сложнее решить, когда базовый тип SInt32. Вы занимаетесь арифметикой и просите решающую программу максимизировать и минимизировать две отдельные цели. Вы можете себе представить, что если у вас есть неограниченныйIntegerзначений, с максимальным сложением чисел может быть легко справиться: по мере увеличения аргументов будет увеличиваться и их сумма. Но это не так дляSInt32: Как только значения начнут переполняться, сумма будет намного меньше, чем аргументы из-за циклического переноса. Таким образом, с модульной арифметикой пространство поиска становится намного интереснее и больше по сравнению сSIntegerкейс. Суть в том, что покаSInt32 имеет конечное представление, задача оптимизации над SInt32 x SInt32 x SInt32 (у вас есть три переменные), может быть намного сложнее из-за того, как работает арифметика по сравнению с SInteger x SInteger x SInteger. В частности, решение надSInt32будет не обязательно быть одинаковым поSIntegerопять же из-за модульной арифметики.

Конечно, то, что происходит за дверьми внутри z3, - это скорее черный ящик, и, возможно, они работают неоправданно медленно. Если вы думаете, что это так, вы могли бы также сообщить об этом людям z3. SBV может сгенерировать стенограмму, которую вы отправите им, если использовать ее следующим образом:

optimizeWith z3{transcript = Just "longRun.smt2"} ...

Это создаст файл longRun.smt2в нотации SMTLib, которую можно передать решателю вне экосистемы Haskell. Вы можете зарегистрировать такую ​​ошибку по адресу: https://github.com/Z3Prover/z3/issues, но имейте в виду, что файлы SMTLib, созданные SBV, могут быть длинными и подробными: если вы можете уменьшить размер проблемы, каким-то образом все еще демонстрируя проблему, это было бы полезно.