Общий случай
Это не просто вопрос эффективности.Рассмотрим проблему, когда у вас есть две переменные a и b и одно ограничение:
a! = B
Каков диапазон b?(максимум или иначе?)
Можно сказать, что все значения являются законными.Но это было бы неправильно, поскольку очевидно, что выбор a влияет на выбор b.Чем больше у вас переменных, тем сложнее станет проблема.Я не думаю, что проблема даже хорошо определена в этом случае, поэтому поиск решения (эффективного или иного) не имеет особого смысла.
Предположение об одной переменной
Сказав, чтоЯ думаю, вы можете найти решение, если предположите, что в системе точно одна переменная.(Или, в качестве альтернативы, если вы фиксируете все другие переменные в некоторых предопределенных константах.) Если вы хотите пойти по этому пути, то вы можете реализовать алгоритм двоичного поиска, чтобы найти диапазон разумного размера, просто доказав квантифицированную формулу
Exists([b], And(b >= minBound, b <= maxBound, Not(constraints)))
Как только вы получите unsat для этого, у вас есть свой диапазон.Пока вы получаете sat, вы можете настроить minBound / maxBound для поиска в меньших диапазонах.В худшем случае это может превратиться в линейную прогулку, но вы можете «урезать» этот поиск, убедившись, что вы уменьшаете значительный размер на каждом шаге.Это может быть параметром для всего поиска, в зависимости от того, насколько большими должны быть ваши интервалы.Это будет выбор между поиском максимального диапазона и тем, сколько времени вы хотите провести в этом поиске.Конечно, если вы урезаете слишком много, вы можете пропустить большой интервал, но это цена эффективности.
Example1 (Хороший случай) Есть одно ограничение, которое говорит b != 5.Тогда ваш поиск будет быстрым, и в зависимости от того, в какую ветку вы пойдете, вы либо найдете [0, 4] или [6, 255], предполагая 8-битные слова.
Example2 (Плохой регистр) Есть одно ограничение: b is even.Тогда ваш поиск будет демонстрировать поведение в худшем случае, и если ваш «урезанный» размер равен 1, вы, возможно, выполните итерацию 255 раз, прежде чем остановитесь на [0, 0];при условии, что z3 дает вам максимальное нечетное число в каждом вызове.
Надеюсь, это иллюстрирует суть.В целом, однако, я бы предположил, что вы будете ближе к «хорошему случаю» для практических приложений, и даже если ваш урезанный размер минимален, вы, скорее всего, сможете сходиться за несколько итераций.Конечно, это полностью зависит от вашей проблемной области, но я ожидаю, что она будет применима для анализа программного обеспечения в целом.