Ответ 1
Одним из способов достижения этого является использование одного из API, а также возможностей генерации модели. Затем вы можете использовать сгенерированную модель из одной проверки выполнимости, чтобы добавить ограничения, чтобы предотвратить использование прежних значений модели в последующих проверках выполнимости, пока не будет выполнено более удовлетворительных заданий. Конечно, вы должны использовать конечные сортировки (или иметь некоторые ограничения, обеспечивающие это), но вы также можете использовать это с бесконечными сортировками, если вы не хотите находить все возможные модели (т.е. Остановитесь после создания группы).
Вот пример использования z3py (ссылка на z3py script: http://rise4fun.com/Z3Py/a6MC):
a = Int('a')
b = Int('b')
s = Solver()
s.add(1 <= a)
s.add(a <= 20)
s.add(1 <= b)
s.add(b <= 20)
s.add(a >= 2*b)
while s.check() == sat:
print s.model()
s.add(Or(a != s.model()[a], b != s.model()[b])) # prevent next model from using the same assignment as a previous model
В общем, использование дизъюнкции всех вовлеченных констант должно работать (например, a и b здесь). Это перечисляет все целые назначения для a и b (между 1 и 20), удовлетворяющими a >= 2b. Например, если мы ограничиваем a и b вместо 1 и 5, то вывод:
[b = 1, a = 2]
[b = 2, a = 4]
[b = 1, a = 3]
[b = 2, a = 5]
[b = 1, a = 4]
[b = 1, a = 5]