Ejercicio 1: Sistemas de ecuaciones sobre enteros

Uno corto

Codificar la siguiente ecuación sobre enteros en Z3 para encontrar una solución:

Uno más largo

Considerar el rompecabezas siguiente:

  1. Hay cinco casas.
  2. El Inglés vive en la casa roja.
  3. El Español posee el perro.
  4. Se toma café en la casa verde.
  5. El Ucraniano toma té.
  6. La casa verde está justo a la derecha de la casa de color marfil.
  7. El fumador de Old Gold posee caracoles.
  8. Se fuman Kools en la casa amarilla.
  9. Se toma leche en la casa del medio.
  10. El Noruego vive en la primera casa.
  11. El que fuma Chesterfields vive en la casa al lado del que tiene un zorro.
  12. Se fuman Kools en la casa al lado de la casa donde hay un caballo.
  13. El fumador de Lucky Strike toma jugo de naranja.
  14. El Japonés fuma Parliaments.
  15. El Noruego vive al lado de la casa azul.

Además, alguien toma agua, alguien posee una zebra, y cada una de las cinco casas está pintada de un color distinto, y sus habitantes son de nacionalidades distintas, poseen mascotas distintas, toman bebidas distintas y fuman distintas marcas de cigarillos.

  1. Codificar cada entidad como un valor entero, representando el número de la casa.
  2. Para definir que el Inglés vive en una casa roja, agregar la restricción siguiente: (= Ingles Rojo).
  3. Tenemos que limitar el valor de todas las casas de tal forma que sea entre 1 y 5.
  4. Para definir que el Noruego vive al lado de la casa azul, no sabemos si vive a la derecha o a la izquierda de esa, pero sabemos que la diferencia entre esos dos números es 1. Entonces agregamos la restricción (or (= Noruego (- Azul 1)) (= Noruego (+ Azul 1))). (Ayuda: en este caso como los otros dados en el enunciado, no hay overflow, o sea esta restricción sirve tal cual sin fijarse que no superemos el valor 5.)
  5. Finalmente usamos (distinct t1 t2 ... tn) para especificar que todas las entidades de mismo tipo (color, casa, etc.) tienen un valor distinto.

Ejercicio 2: vectores de bits

Documentación

Un equivalente extraño de la función XOR

Considerá la operación siguiente: (x + y - ((x & y) << 1)) donde << n es la operación "shift left n veces".

Demostrá que esta operación es equivalente a la operación x xor y sobre cualquier par (x, y) de vectores de bits de tamaño 64.

Ayuda: el vector de 64 bits que contiene solo el valor 1 se puede escribir directamente (_ bv1 64)).

Vulnerar un generador pseudoaleatorio de números

El generador pseudoaleatorio por defecto de la librería estándar de C es basado sobre un LCG (Linear Congruential Generator). Sus debilidades son conocidas, veamos si podemos encontrar sus valores de estados interno solo viendo la salida de un programa y conociendo la implementación del LCG. Vamos a definir las relaciones entre los estados internos del LCG usando Z3. Este es un programa de prueba:

#include <stdlib.h>
#include <stdio.h>
#include <time.h>
main(){
  int i;
  srand(time(NULL));
  for (i=0; i<10; i++)
    printf ("%d\n", rand()%100);
}

Imprime 10 números entre 0 y 99:

37
29
74
95
98
40
23
58
61
17

Definamos obs2 = 29, obs3 = 74, obs9 = 61.

Veamos si observando solo 8 valores (de 29 a 61) podemos predecir el siguiente (17).

Este programa está compilado con MSVC 2013 (su LCG es más simple que el de GLib). Usemos un desensemblador para conocer las operaciones y constantes que usa:

.text:0040112E rand    proc near
.text:0040112E         call __getptd
.text:00401133         imul ecx, [eax+0x14], 214013
.text:0040113A         add  ecx, 2531011
.text:00401140         mov  [eax+14h], ecx
.text:00401143         shr  ecx, 16
.text:00401146         and  ecx, 7FFFh
.text:0040114C         mov  eax, ecx
.text:0040114E         retn
.text:0040114E rand    endp

Estamos listos para usar Z3.

  1. Declarar vectores de bits de tamaño 32 llamados state1 a state10, output_prev y output_next.
  2. Agregar las aserciones siguientes que conectan los estados internos consecutivos del LCG:
  3. Agregar las aserciones siguientes que conecta los estados internos del LCG con los valores observados en la salida del programa ejecutable:
  4. Agregar las últimas aserciones:
  5. Comprobar que Z3 encuentra los valores siguientes:
sat
[state3 = 2276903645,
 state4 = 1467740716,
 state5 = 3163191359,
 state7 = 4108542129,
 state8 = 2839445680,
 state2 = 998088354,
 state6 = 4214551046,
 state1 = 1791599627,
 state9 = 548002995,
 output_next = 17,
 output_prev = 37,
 state10 = 1390515370]
Por defecto, Z3 muestra los vectores de bits sin convertirlos a enteros.
Para que Z3 muestre los vectores de bits como enteros, agregar
lo siguiente a la fórmula: `(set-option :pp.bv-literals false)`.
  1. Seguramente tu fórmula contiene mucho código repetido. Definí funciones para evitar esas repeticiones.