Un acertijo es un sistema de ecuaciones booleanas
Codifica a quien dice la verdad como 1 y al mentiroso como 0. Hay coherencia cuando el valor de su frase coincide con su bit de rol.
SX(R) = RX
El laboratorio comprueba S_X(R) = R_X para cada X. Todas las ecuaciones comparten el mismo vector R y deben cumplirse a la vez.
Cada frase es una función booleana de la asignación completa.
Una contradicción elimina todo un mundo posible
Supón una asignación, evalúa cada frase y compara el resultado con el rol del hablante.
SX(R) ≠ RX ⇒ reject R
Una sola discrepancia basta para rechazar la asignación. Las pistas identifican el supuesto y la ecuación que vuelve imposible su rama.
La contradicción demuestra que un mundo no puede satisfacer las reglas.
No basta con que sea resoluble: debe ser único
Un acertijo puede ser coherente y aun tener varias asignaciones válidas.
|{R : ∀X, SX(R)=RX}| = 1
Cada acertijo generado se comprueba exhaustivamente y solo se acepta si sobrevive exactamente un mundo.
El mundo verde es el único modelo del sistema.
Las pistas fuertes eliminan muchos mundos
Una frase útil divide los candidatos; una débil puede valer igual en casi todos.
candidates: 2n → … → 1
El motor de pistas elige la ecuación no aplicada que elimina más mundos actuales: reduce incertidumbre sin saltar a la respuesta.
El número de candidatos baja con ecuaciones informativas.
La autorreferencia no siempre es una pista útil
«Digo la verdad» concuerda con ambos roles y no aporta información.
SX(R) = RX
«Estoy mintiendo» no puede decirlo coherentemente ningún rol bajo reglas estrictas. El generador excluye ambos patrones y usa relaciones entre participantes.
Una autoafirmación es tautológica; la otra crea una ecuación imposible.