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

Question

Я хотел бы использовать 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?

Answer 1

То, что вы делаете, по сути, так же, как и в 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.true", "-v3"]} $ do ...

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

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

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

• satConcurrentWithAny
• satConcurrentWithAll
• verifyConcurrentWithAny
• verifyConcurrentWithAll

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