Използване на 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 config, можете да видите какви са те, като издадете 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