Ускорьте построение формулы в Z3Py - PullRequest
Новая
       36

Ускорьте построение формулы в Z3Py

0 голосов
/ 28 апреля 2019

Я использую Z3Py для построения больших формул (~ 1500 Bool переменных, ~ 90k утверждений), и в настоящее время я использую Solver.add для добавления утверждений, которые в основном невелики (например, последствия для 2 переменных).

Мой код выглядит примерно так: примерно 10 внешних for последовательностей.Глубина вложения цикла варьируется от 2 до 6. 

s = Solver()

for i in range(A):
  for j in range(B):
    ...
      s.add(Implies(vars[i,j,...], vars[k,l,...]))

Проблема в том, что построение решателя занимает ~ 11 секунд (с __debug__ == False), а на поиск решения - всего около 8.

Профилирование показывает, что много времени тратится на Z3_sort_to_ast, z3code.Elementaries.Check (вызываемый первым) и другие методы, которые, как кажется, могут быть встроены по крайней мере, если не исключены каким-либо образом.

Как оптимизировать создание Z3 Solver?Может быть, есть внутренний интерфейс более низкого уровня, который может ускорить процесс?

1 Ответ

2 голосов
/ 28 апреля 2019

Я вижу 3 варианта:

  • Использование интерфейса SMT-LIB
  • Пропустить высокоуровневый API Z3
  • Переписать код, используя C APIнапрямую

Если взаимодействие с Z3 минимально (решить и получить модель), SMT-LIB может быть лучшим вариантом.

Если код Python достаточно сложен для перезаписи вC, пожалуйста, попробуйте pySMT.Способ, которым мы интегрируемся с Z3, пропускает высокоуровневый API и вызывает непосредственно базовые C-функции, предоставляемые на уровне python.Из-за самого pySMT может возникнуть дополнительная нагрузка, но обычно она окупается.Вы можете посмотреть на [1] некоторые идеи о том, как мы это делаем.

[1] https://github.com/pysmt/pysmt/blob/master/pysmt/solvers/z3.py#L853

...