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

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

5 голосов
/ 26 февраля 2020

В попытке выучить Z3 я попытался решить одну из моих любимых задач Advent of Code (особенно сложную, 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 минут go и считая).

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

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

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

1 Ответ

5 голосов
/ 26 февраля 2020

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

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

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

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

...