Как заставить z3py показывать несколько ответов, если это так?

Этот вопрос возникает часто, и есть несколько предостережений. По сути, вам нужно написать цикл, чтобы отклонить более ранние модели и продолжать запрашивать выполнимость. Для вашей конкретной проблемы вы можете закодировать это следующим образом:

from z3 import *

p = Int('p')
q = Int('q')

s = Solver()
s.add(Or(p==1,p==2,p==3), Or(q==1,q==2), Not(p==q), q==1)

res = s.check()
while (res == sat):
  m = s.model()
  print(m)
  block = []
  for var in m:
      block.append(var() != m[var])
  s.add(Or(block))
  res = s.check()

Когда я запускаю это, я получаю:

[p = 2, q = 1]
[p = 3, q = 1]

Обратите внимание, что z3 не всегда создает полную модель: он перестанет создавать назначения, как только определит, что проблема sat. Таким образом, вам, возможно, придется отслеживать свои переменные и явно использовать завершение модели. См. Попытка найти все решения к логической формуле с использованием Z3 в python, чтобы узнать, как это сделать.