Альтернатива z3 для функции Gecode branch ()?

Question

В решателе ограничений, таком как Gecode, мы можем контролировать исследование пространства поиска с помощью функции ветвления. например, branch(home , x , INT_VAL_MIN ) Это начнет исследование пространства поиска с минимально возможного значения переменной x в своем домене и попытается найти решение. (Есть много таких альтернатив.)

Есть ли у нас это для z3 какая-то встроенная гибкость ?? Возможна любая альтернатива ??

Answer 1

Решатели SMT обычно не позволяют давать такого рода «подсказки», они действуют скорее как черные ящики. * 1001 имеет ряд настроек, с которыми вы можете играть, чтобы давать подсказки. Если вы запустите:

z3 -pd

, он отобразит все параметры, которые вы можете предоставить, а их буквально более 600! К сожалению, эти параметры не очень хорошо документированы, и их влияние на решатель довольно сложно c. Единственный надежный способ узнать это - изучить исходный код и посмотреть, что они делают, что не для слабонервных. Но в любом случае это будет не так очевидно, как функция ветвления, которую вы цитируете для gecode.

Однако есть и другие уловки, которые можно использовать для ускорения решения для SMT-решателей, к сожалению, это обычно очень проблемные c. Если вы опубликуете конкретные c экземпляры, вы можете получить лучшие предложения.