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