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

Question

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

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

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

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

Answer 1

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

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

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

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