Use Z3 y Smtlib para calcular la configuración/modelo con valores mixtos
Pregunta
¿Cómo calculo los valores atribuidos? Aquí hay un ejemplo:
(declare-fun x () bool)
(declare-fun y () bool)
(declare-fun z () bool)
(assert (AND x (OR y z)))
Con esto obtendría 2 modelos:
x=true and y=true
x=true and z=true
Ahora, lo que quiero es algo como esto:
(declare-fun x () bool)
(declare-fun y () bool)
(declare-fun z () bool)
(declare-fun x.val () Int)
(declare-fun y.val () Int)
(declare-fun z.val () Int)
(assert (= x.val 2))
(assert (= y.val 3))
(assert (= z.val 5))
(assert (AND x (OR y z)))
(assert (> sum 6))
Entonces, me gustaría obtener el modelo donde la suma de los atributos es mayor que 6:
x=true and z=true
Tal vez trabajar con matrices es una forma de lograr esto ...
Solución
No estoy seguro de si entendí tu pregunta correctamente. Parece que desea asociar un atributo (entero) a cada variable booleana. Entonces, cada variable es un par: un valor booleano y un atributo entero. Supongo que por sum
, quiso decir la suma de los atributos de las variables asignadas a verdaderas. Si ese es el caso, puede modelarlo en Z3 de la siguiente manera:
;; Enable model construction
(set-option :produce-models true)
;; Declare a new type (sort) that is a pair (Bool, Int).
;; Given a variable x of type/sort WBool, we can write
;; - (value x) for getting its Boolean value
;; - (attr x) for getting the integer "attribute" value
(declare-datatypes () ((WBool (mk-wbool (value Bool) (attr Int)))))
;; Now, we declare a macro int-value that returns (attr x) if
;; (value x) is true, and 0 otherwise
(define-fun int-value ((x WBool)) Int
(ite (value x) (attr x) 0))
(declare-fun x () WBool)
(declare-fun y () WBool)
(declare-fun z () WBool)
;; Set the attribute values for x, y and z
(assert (= (attr x) 2))
(assert (= (attr y) 3))
(assert (= (attr z) 5))
;; Assert Boolean constraint on x, y and z.
(assert (and (value x) (or (value y) (value z))))
;; Assert that the sum of the attributes of the variables assigned to true is greater than 6.
(assert (> (+ (int-value x) (int-value y) (int-value z)) 6))
(check-sat)
(get-model)
(assert (not (value z)))
(check-sat)
Otros consejos
Con tres variables, imagino que sería algo así:
(define-fun cond_add ((cond Bool) (x Int) (sum Int)) Int
(ite cond (+ sum x) sum))
(declare-fun sum () Int)
(assert (= sum (cond_add x x.val (cond_add y y.val (cond_add z z.val 0)))))
(assert (> sum 6))
Aquí defino una macro cond_add
Para agregar una variable a un acumulador cuando se mantiene una condición correspondiente. Y sum
se define para tener en cuenta la suma condicional de x.val
, y.val
y z.val
basado en valores de verdad de x
, y
y z
.