Использование Z3 с распараллеливанием от SBV

Я хотел бы использовать Z3 через SBV с использованием нескольких ядер. Основываясь на этом ответе, я смогу сделать это, просто передав parallel.enable=true исполняемому файлу z3 в командной строке. Поскольку я использую SBV, мне нужно пройти через интерфейс SBV к различным решателям SMTLib, поэтому вот что я пробовал:

foo = runSMTWith z3par $ do
    ...
  where
    z3par = z3
        { SBV.solver = (SBV.solver z3)
              { SBV.options = \cfg -> SBV.options (SBV.solver z3) cfg ++ ["parallel.enable=true"]
              }
        }

Однако я не вижу никаких признаков того, что Z3 работает с включенным распараллеливанием:

  • Использование процессора не превышает одного ядра
  • Нет ускорения по сравнению с запуском без этого флага

Как включить распараллеливание Z3 при переходе через SBV?


haskell z3 sbv
person Cactus    schedule 30.07.2020    source источник

Ответы (1)


arrow_upward
2
arrow_downward

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

import Data.SBV
import Data.SBV.Control

foo :: IO (Word64, Word64)
foo = runSMTWith z3{solver = par} $ do
        x <- sWord64 "x"
        y <- sWord64 "y"

        setOption $ DiagnosticOutputChannel "diagnostic_output"

        constrain $ x * y .== 13
        constrain $ x .> 1
        constrain $ y .> 1

        query $ do ensureSat
                   (,) <$> getValue x <*> getValue y

  where par    = (solver z3) {options = \cfg -> options (solver z3) cfg ++ extras}
        extras = [ "parallel.enable=true"
                 , "-v:3"
                 ]

Здесь мы не только настраиваем параллельный режим z3, но также сообщаем ему, чтобы он увеличил уровень детализации и поместил все диагностические данные в файл. (Примечание: в параллельном разделе конфигурации z3 есть много других настроек, вы можете увидеть, что они из себя представляют, введя z3 -pd в своей командной строке и просмотрев вывод. Вы можете установить любые другие параметры оттуда, добавив их в extras переменная выше.)

Когда я запускаю вышеуказанное, я получаю:

*Main> foo
(6379316565415788539,3774100875216427415)

Но я также получаю файл с именем diagnostic_output, созданный в текущем каталоге, который содержит среди прочего следующие строки:

(tactic.parallel :progress 0%  :open 1)
(tactic.parallel :split-cube 0)
(parallel.tactic simplify-1)
(tactic.parallel :progress 100.00% :status sat :open 0)

Итак, z3 действительно находится в параллельном режиме, и все происходит. Конечно, то, что именно он делает, является более или менее черным ящиком, и невозможно интерпретировать приведенный выше вывод, не проверив внутренности z3. (Я не думаю, что значение этой статистики или стратегии для параллельного решателя так хорошо задокументированы. Если вы найдете хорошую документацию по деталям, пожалуйста, сообщите!)

Обновлять

После этого фиксации вы можете просто сказать:

runSMTWith z3{extraArgs = ["parallel.enable=true"]} $ do ...

еще больше упрощая программирование.

Независимый от решателя параллелизм непосредственно из SBV

Обратите внимание, что в SBV также есть комбинаторы для одновременного запуска вещей непосредственно из Haskell. См. функции:

Эти функции не зависят от решателя, вы можете использовать их с любым решателем по вашему выбору. Конечно, они требуют, чтобы вы реструктурировали свою проблему и выполнили ручную декомпозицию, чтобы воспользоваться преимуществами многоядерности вашего компьютера и собрать решения вместе самостоятельно. Но они также дают вам полный контроль над тем, как вы хотите структурировать свой дорогостоящий поиск.

person alias    schedule 30.07.2020