Une énigme est un système d'équations booléennes
Codez le véridique par 1 et le menteur par 0. Un locuteur est cohérent si la valeur de sa phrase égale son bit de rôle.
SX(R) = RX
Le laboratoire vérifie S_X(R) = R_X pour chaque X. Toutes les équations partagent le même vecteur R et doivent tenir ensemble.
Chaque phrase est une fonction booléenne de l'attribution complète.
Une contradiction élimine tout un monde possible
Supposez une attribution, évaluez chaque phrase et comparez le résultat au rôle du locuteur.
SX(R) ≠ RX ⇒ reject R
Un seul écart suffit à rejeter l'attribution. Les indices nomment l'hypothèse et l'équation qui rend sa branche impossible.
La contradiction démontre qu'un monde ne peut satisfaire les règles.
Être soluble ne suffit pas : la réponse doit être unique
Une énigme peut être cohérente tout en ayant plusieurs attributions valides.
|{R : ∀X, SX(R)=RX}| = 1
Chaque énigme est vérifiée exhaustivement et acceptée seulement si un seul monde survit.
Le monde vert est l'unique modèle du système.
Les indices forts éliminent beaucoup de mondes
Une phrase utile partage les candidats ; une faible vaut pareil dans presque tous.
candidates: 2n → … → 1
Le moteur choisit l'équation non appliquée qui retire le plus de mondes : il réduit l'incertitude sans donner directement la réponse.
Les candidats diminuent avec les équations informatives.
L'autoréférence n'est pas automatiquement utile
« Je dis la vérité » convient aux deux rôles et n'apporte aucune information.
SX(R) = RX
« Je mens » ne peut être dit de façon cohérente par aucun rôle strict. Le générateur exclut les deux formes et utilise des relations entre participants.
Une autoaffirmation est tautologique ; l'autre crée une équation impossible.