Я использую z3py для решения набора уравнений. Как бы вычислить его время выполнения? Он имеет переменные битвеков, которые должны выполняться в наборе линейных уравнений. Документация и руководство не дают возможности рассчитать время выполнения.как вычислить время выполнения Z3 sat solver
0
A
ответ
1
Вы запрашиваете (худший вариант) временная сложность использованных решателей? Если это так, я не думаю, что вы сможете получить хороший ответ: это зависит от (комбинации) логики (ов), в которые падает ваша проблема, например. QF_BV или UFNIA, а затем в процедурах ((полу) решения), которые решатель реализует для этой (комбинации) логики (ов).
Посмотрите документы от авторов Z3 (https://github.com/Z3Prover/z3/wiki/Publications) - они могут предоставить некоторые детали.
Смежные вопросы
- 1. Случайное семя для Z3 SAT Solver
- 2. Prolog SAT Solver
- 3. Z3 Время ожидания с помощью Solver
- 4. Копирование Z3 Solver
- 5. SAT Solver: SAT4J - еще примеры?
- 6. Microsoft Solver Foundation SAT CNF
- 7. Как скомпилировать глюкометр SAT solver на Mac?
- 8. z3 solver: z3-SMT на платформе Mac
- 9. Prolog - jigoku solver - время выполнения
- 10. Z3 4.0 Push and Pop In Solver
- 11. Simplfying Expression: Z3 SMT Solver
- 12. SAT solver set default result (cryptominisat)
- 13. Как вычислить среднее время выполнения?
- 14. Проблемы с использованием Z3 для MAX-SAT
- 15. Вызов внешнего SAT-решателя от Z3
- 16. Вычислить время выполнения cron
- 17. Picosat SAT solver: установить предел распространения - но какое значение?
- 18. Microsoft Z3 Dot Net API, Cloning Solver
- 19. Z3 Solver: Стабильная версия для Java API
- 20. Скорость z3-solver с правильной тактикой
- 21. Z3 добавление новых переменных во время выполнения
- 22. Вычислить время для выполнения функции
- 23. (check-sat) vs (check-sat-using smt)
- 24. вычислить время выполнения моей программы
- 25. Есть ли wbo-подобный SAT-Solver для Python?
- 26. Как вычислить сложность алгоритма, имея время выполнения?
- 27. Вычислить минимальное значение Bitvector в Z3
- 28. Как оценить время, затрачиваемое на решение SAT в z3 для SMT?
- 29. Анализ времени выполнения Z3
- 30. Как создать интерфейс для объекта solver и использовать его (Z3 solver)