¿Puede un cliente pagar menos de 35 euros?
Un solver como Z3 es un programa al que le das reglas y te dice si existen valores que las cumplen. Sirve para comprobar una afirmación en todos los casos a la vez, sin probarlos uno a uno.
Una tienda online descuenta 5 euros de los pedidos de 40 euros o más. ¿Puede alguien pagar menos de 35 euros? Z3 contesta sin probar ni un solo pedido.
Al final de esta lección
Nota
Puedo preguntar a Z3 si una afirmación se cumple siempre.
Palabras clave
| Palabra | Qué significa | Ejemplo |
|---|---|---|
| Solver | un programa que busca valores que cumplan unas reglas | |
| Satisfacible (sat) | las reglas tienen al menos una solución | |
| Insatisfacible (unsat) | las reglas no tienen ninguna solución | |
| Modelo | una solución concreta que da el solver | x = 11 |
| Negación | lo contrario de una afirmación | |
| Regla | una condición que los valores deben cumplir | price >= 40 |
Las celdas que rellenan los estudiantes quedan en blanco en esta vista previa.
Z3 contesta sat o unsat
Le das a Z3 una lista de reglas y le preguntas: ¿hay algún valor que las cumpla todas? Hay dos respuestas posibles.
sat quiere decir que sí. Z3 puede enseñarte un valor concreto, el modelo. unsat quiere decir que no existe ninguno.
Cómo se escribe una regla en Z3
| En matemáticas | En Z3 | Qué significa |
|---|---|---|
| x > 10 | (> x 10) | x es mayor que 10 |
| price - 5 | (- price 5) | el precio menos 5 |
| no (x > 10) | (not (> x 10)) | lo contrario de la regla |
| x es un entero | (declare-const x Int) | crea la variable x |
Las celdas que rellenan los estudiantes quedan en blanco en esta vista previa.
Dos reglas que sí se pueden cumplir
echo '(declare-const x Int) (assert (> x 10)) (assert (< x 13)) (check-sat) (get-value (x))' | z3 -inSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Dos reglas que se contradicen
echo '(declare-const x Int) (assert (> x 10)) (assert (< x 11)) (check-sat)' | z3 -inSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Se demuestra pidiendo lo contrario
Para comprobar una afirmación, se la niega y se le pide a Z3 un caso que la cumpla. Es decir, un caso donde la afirmación original falle.
Si Z3 contesta unsat, ese caso no existe y la afirmación vale siempre. Si contesta sat, el modelo que enseña es un contraejemplo.
Ejemplo: el descuento de 5 euros
| Paso | Contenido |
|---|---|
| Regla | el pedido cuesta 40 euros o más: price >= 40 |
| Afirmación | tras restar 5 se paga al menos 35: price - 5 >= 35 |
| Negación | se paga menos de 35: not (price - 5 >= 35) |
| Pregunta a Z3 | regla y negación a la vez, ¿hay solución? |
| Respuesta esperada | unsat: la afirmación vale para todo precio |
Las celdas que rellenan los estudiantes quedan en blanco en esta vista previa.
Demuestra que se paga al menos 35
echo '(declare-const price Int) (assert (>= price 40)) (assert (not (>= (- price 5) 35))) (check-sat)' | z3 -inSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Prueba una afirmación falsa: al menos 36
echo '(declare-const price Int) (assert (>= price 40)) (assert (not (>= (- price 5) 36))) (check-sat) (get-value (price))' | z3 -inSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Un error frecuente
Advertencia
Mucha gente lee sat como "la afirmación es cierta". Pero lo que se le pregunta a Z3 es la negación. Si sobre la negación Z3 dice sat, existe un contraejemplo y la afirmación es falsa. La afirmación queda demostrada cuando dice unsat.
Enteros y decimales no dan lo mismo
La variable tiene un tipo, y el tipo cambia la respuesta. En los enteros, x * x >= x se cumple siempre. Con decimales, no: para la mitad, 0,5 * 0,5 es 0,25, que es menor que 0,5.
Antes de fiarte de un resultado, mira con qué tipo declaraste la variable.
La misma afirmación con decimales
echo '(declare-const x Real) (assert (not (>= (* x x) x))) (check-sat)' | z3 -inSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.