Z3: encontrando todos los modelos satisfactorios

smt theorem-proving

Question

Estoy intentando recuperar todos los modelos posibles para una teoría de primer orden utilizando Z3, un solucionador de SMT desarrollado por Microsoft Research. Aquí hay un mínimo ejemplo de trabajo:

(declare-const f Bool)
(assert (or (= f true) (= f false)))

En este caso proposicional hay dos asignaciones satisfactorias: f->true y f->false . Debido a que Z3 (y los solucionadores de SMT en general) solo intentarán encontrar un modelo satisfactorio, no es posible encontrar todas las soluciones directamente. Here encontré un comando útil llamado (next-sat) , pero parece que la última versión de Z3 ya no lo admite. Esto es un poco desafortunado para mí, y en general creo que el comando es bastante útil. ¿Hay otra manera de hacer esto?

Answer 1

Una forma de lograr esto es usar una de las API, junto con la capacidad de generación de modelos. Luego, puede usar el modelo generado de una verificación de satisfacción para agregar restricciones para evitar que los valores del modelo anterior se usen en las verificaciones de satisfacción posteriores, hasta que no haya más asignaciones satisfactorias. Por supuesto, debe usar clasificaciones finitas (o tener algunas restricciones que lo aseguren), pero también podría usarlas con infinitas clasificaciones si no desea encontrar todos los modelos posibles (es decir, detenerse después de generar un montón) .

Aquí hay un ejemplo utilizando z3py (enlace a la secuencia de comandos de z3py: 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

En general, usar el disyuntivo de todas las constantes involucradas debería funcionar (por ejemplo, a y b aquí). Esto enumera todas las asignaciones de enteros para a y b (entre 1 y 20 ) que satisfacen a >= 2b . Por ejemplo, si restringimos a y b para que se ubiquen entre 1 y 5 , la salida es:

[b = 1, a = 2]
[b = 2, a = 4]
[b = 1, a = 3]
[b = 2, a = 5]
[b = 1, a = 4]
[b = 1, a = 5]