Z3 возвращает неизвестный

У меня есть простой набор ограничений, с которыми Z3 не справляется:

http://pastebin.com/3eaLQ9wx

Есть ли способ настроить ограничения, чтобы получить результат? Это простой пример большего набора ограничений (тысячи), но меня как-то беспокоит, что он не работает даже на таком простом примере.

Заранее спасибо !!


z3 smt
person user1217406    schedule 31.12.2012    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Ваша проблема имеет нелинейные ограничения. В то время как Z3 может справиться с ними в большинстве случаев, смешивание Ints и Real, кажется, ставит его за пределы его текущих возможностей. Если вы просто используете Reals для своих переменных s_0_1, s_0_2 и т. д., я верю, что Z3 сможет решить проблему. (Кажется, у вас достаточно ограничений по значениям, поэтому я надеюсь, что проблем с моделированием не возникнет.)

Думаю, Леонардо несколько раз говорил, что в следующих релизах будет лучше поддерживаться комбинированная теория при наличии нелинейных ограничений.

person alias    schedule 31.12.2012
comment
Левент прав, проблема заключается в использовании смешанной целочисленной и действительной нелинейной арифметики. Я вижу два возможных обходных пути. Мы можем заменить все целочисленные переменные реальными переменными, это нормально, так как целочисленные переменные могут принимать только значения 0 или 1 в вашей задаче (вот это решение: rise4fun.com/Z3Py/ICFA). В этом случае будет использоваться новый решатель nlsat в Z3. Другой вариант — заменить целочисленные переменные булевыми и линеаризовать задачу с помощью Ifs. Вот ссылка на это решение rise4fun.com/Z3Py/egCe. Второе решение должно лучше масштабироваться. - person Leonardo de Moura; 31.12.2012