В решателе ограничений, таком как Gecode, мы можем контролировать исследование пространства поиска с помощью функции ветвления. например branch(home , x , INT_VAL_MIN ) Это начнет исследование пространства поиска с минимально возможного значения переменной x в его домене и попытается найти решение. (Таких альтернатив много.)
Для z3 у нас есть такая встроенная гибкость?? Возможна любая альтернатива??
Решатели SMT обычно не позволяют давать такого рода «подсказки», они действуют скорее как черные ящики.
Сказав это, каждый решатель использует массу внутренних эвристик, а сам z3 имеет ряд настроек, с которыми вы можете играть, чтобы дать ему подсказки. Если вы запустите:
z3 -pd
он отобразит все варианты, которые вы можете предоставить, а их буквально более 600! К сожалению, эти параметры не очень хорошо задокументированы, и то, как они влияют на решатель, довольно загадочно. Единственный надежный способ выяснить это — изучить исходный код и посмотреть, что они делают, что не для слабонервных. Но в любом случае это будет не так очевидно, как приводимая вами фича ветки для gecode.
Однако есть и другие приемы, которые можно использовать для ускорения решения SMT-решателей, к сожалению, эти вещи обычно очень специфичны для конкретной задачи. Если вы опубликуете конкретные экземпляры, вы можете получить лучшие предложения.
