Задача
Я пытаюсь использовать z3 для опровержения утверждений о достижимости в сети Петри.
Итак, я объявляю N переменных состояния v0, .. v_n-1, которые являются натуральными числами, по одной на каждое место в сети Петри.
Моя основная стратегия с учетом атомарного предложения P о состояниях такова:
- вычисляет (с внешним механизмом) любые «легкие» положительные инварианты в виде линейных ограничений на переменные в форме alpha_0 * v_0 + ... = постоянная только с положительным или нулевым alpha_i, затем check_sat, если любое состояние, достижимое при этих ограничения удовлетворяют P, если не удовлетворены, в противном случае
- вычислить (внешне для z3) обобщенные инварианты, где alpha_i также может быть отрицательным, а check_sat - в случае несоответствия, в противном случае
- добавить одну положительную переменную t_i на каждый переход системы и утвердить уравнение состояния сети Петри, чтобы любое достижимое состояние имело вектор счетчика зажигания Париха (значение t_i), такой что M0 - начальное состояние + произведение этого вектора Париха. Матрица инцидентности дает достигнутое состояние. Так что этот вводит много новых переменных и включает в себя некоторое умножение переменных, но остается проблемой линейного целочисленного программирования.
Я разделяю шаги, потому что, поскольку я хочу UNSAT, любой check_sat, который возвращает UNSAT, останавливает процедуру, и последний шаг, в частности, очень дорогой.
У меня проблемы с более крупными моделями, когда я получаю непомерно большое время ответа или даже ужасный «неизвестный» ответ, особенно при добавлении уравнения состояния (шаг 3).
Фон
Поэтому, помимо разделения задачи на постепенно усложняющиеся сегменты, я попытался установить логику QF_LRA, а не QF_LIA, и объявить переменные как вещественные, а не целые числа.
Это избыточное приближение является дружественным к вычислениям (z3 работает быстро на них!), Но, к сожалению, для многих моделей решения не являются целыми, и при этом нет целочисленного решения.
Итак, я попытался установить Reals, но указав, что каждая переменная имеет значение = 0 или> = 1, чтобы удалить решения с долями срабатываний <1. Это исключает ложные решения, но «убивает» z3 (тайм-аут или неизвестно) во многих случаях проблема, очевидно, намного сложнее (например, сложнее, чем с целыми числами). </p>
Примеры
У меня нет небольшого примера, который можно показать, хотя я могу легко его привести. Проблема в том, что если я выберу QF_LIA, он будет слишком медленным при некотором количестве переменных. Как метрика, переходов намного больше, чем мест, поэтому добавление уравнения состояния действительно увеличивает число переменных.
Этот код генерирует примеры, о которых я спрашиваю.
Это общее представление слайды 5 и 6 отражают проблему, которую я кодирую точно, а слайды 7 и 8 демонстрируют результаты того, что дает нам "unsat", если вы хотите больше математического фона.
Я генерирую проблемы из Model Check Contest , с тысячами мест (первичными переменными) и в некоторых случаях более ста тысяч переходов. Это экстремум, средний диапазон - несколько тысяч мест, и, возможно, 20 тысяч переходов, с которыми мне бы очень хотелось иметь дело.
Реально + ограничение больше 1 не является хорошим решением даже для небольших задач. Целые числа медленно с самого начала.
Я мог бы попробовать Reals, а затем итерацию в Integer, если я получу нецелое решение, я не пробовал этого, хотя это предполагает довольно много убийств и перезапуска решателя, это может быть достойным подходом в моем наборе тестов.
Что я ищу
Я ищу некоторые настройки для Z3, которые могли бы лучше помочь ему справиться с проблемами, которыми я питаюсь, дать ему некоторое представление.У меня есть некоторая априорная идея о том, что могло бы решить эти проблемы, традиционно они были переданы специалистам ILP. Поэтому я надеюсь запустить какой-нибудь симплекс, но, возможно, существуют условия, мешающие z3 использовать «хорошую» стратегию решения в некоторых случаях.
Я стал пользователем SMT / Z3 достойного уровня, но я никогда не играл с хорошими настройками: параметров, чтобы помочь солверу.
Кто-нибудь из вас пытался передать SMT основные проблемы ILP и нашел настройки параметров или конкретные кодировки, которые помогут ему развернуть правильные решения? спасибо.