, поэтому я пытаюсь решить проблему планирования, используя z3. У меня есть набор заданий, которые необходимо выполнить, и набор ресурсов, которые могут выполнять эти задания. Задания упорядочены (общий порядок), и в общем случае проблема выражается с использованием линейных арифметических уравнений (=, <,>) и логических выражений (например, задания1 и задания2, распределенные по разным ресурсам => они могут выполняться параллельно).
Сами ограничения не являются сложными, но количество ограничений, которые я добавляю в решатель, исчисляется тысячами и может увеличиться в 10 раз.
Итак, одна из проблем, с которыми я сталкиваюсь, заключается в том, что Z3 кажется не детерминированным в том, как он пытается решить одну и ту же проблему (но во время разных прогонов). Иногда это дает результат в течение нескольких секунд, но иногда это требует времени. То, что я затем часто делаю, это убивает текущий запуск и перезапускает, а затем он снова дает мне результат почти мгновенно.
Мне было интересно, поможет ли использование определенных стратегий / тактик направить Z3 в правильном направлении более последовательно?
Я использую z3py (с оптимизацией), и когда я печатаю (len (z3.tactics ())), я вижу, что есть 107 различных тактик. И если я распечатаю описания этих тактик, используя print (z3.tactics ()), это будет довольно сложно.
Кто-нибудь знает бумагу / веб-сайт, который может подсказать мне, какую тактику использовать в зависимости от того, какие ограничения я использую? (в моем случае: линейная арифметика и некоторые логические ограничения без квантификаторов)