Должно ли введение дополнительных ограничений улучшить время решения для решателей SMT?

Question

У меня есть приложение SMT (построено на библиотеке Haskell SBV), которое решает некоторые сложные уравнения против одного s переменная в реальной логике с использованием Z3. Поиск решения занимает около 30 секунд в моем случае.

Пытаясь ускорить процесс, я добавил дополнительные ограничения s < 40000, так как у меня есть некоторая оценка решения. Я думал, что такое ограничение уменьшит пространство поиска и заставит решатель быстрее вернуть результат. Однако, это только сделало это медленнее (это даже не закончилось через 10 минут).

Вопрос в следующем: можно ли предположить, что дополнительные ограничения всегда замедляют / ускоряют процесс решения или нет общих правил, и это всегда зависит от обстоятельств?

Я обеспокоен тем, что даже мой 30-секундный алгоритм может содержать некоторые дополнительные ограничения, которые не обязательно нужны, а просто замедляют процесс.

Answer 1

Я не думаю, что вы можете сделать какие-либо общие предположения по этому поводу. Это может или не может повлиять на время решения, предполагая, sat/unsat статус не меняется.

Равенства, как правило, помогают (так как они распространяются свободно), но для всего остального никто не догадывается. Кроме того, разные решатели могут демонстрировать различное поведение для одного и того же дополнения.

Один из способов думать об этом заключается в том, что лежащий в основе алгоритм DPLL(T), по сути, является очень умным прославленным алгоритмом поиска. Он продолжает выпускать "выученные леммы" в надежде, что найдет противоречие с ранее известным фактом. Новое "ограничение", которое вы добавите, может привести к генерации тонны правильных, но не относящихся к делу лемм, которые приведут его к глубокому концу без какого-либо полезного результата. (Количественные формулы, как правило, выглядят следующим образом: вы можете создавать их миллионами разных способов; но если вы не найдете "правильную" реализацию, все, что они сделают, это в конечном итоге загрязнит ваше пространство поиска.)

По крайней мере, это был мой опыт!