Решатели Z3 выводят CUT 2 - PullRequest
       7

Решатели Z3 выводят CUT 2

0 голосов
/ 09 января 2019

Я работаю над сложной проблемой картирования. Чтобы получить все Парето-оптимальные решения, я использовал мод Парето Z3. Когда я удалил некоторые ограничения, некоторые проволочные вещи произошли, что не должно влиять на решения, но решений было на одно меньше. Когда последний найдет Z3, выведите «CUT 2» и не нашли последнее решение. Так что значит "CUT 2"? Это как-то связано с отсутствием решения?

...