L’implication fait partie des techniques avancées. Elle fonctionne avec des booléens et demande la mise en place d’hypothèses. Elle produit une simplification du nombre de booléens.

Soient a et b deux booléens.

Si a=>b et b=>a, alors a<=>b

La règle est on ne peut plus simple. Pour la mettre en œuvre on commence par le booléen a et on suppose qu’il est vrai. Si on constate que le booléen b devient vrai à la suite de a, nous avons démontré que :

a => b

Alors, il faut remettre les grilles dans leur état d’origine et reprendre le même travail avec b: on suppose que b est vrai. Si on constate que le booléen a devient vrai par la suite, nous avons démontré que :

b => a

De ce fait, les deux booléens a et b sont équivalents : a <=> b , et on peut remplacer l’un par l’autre.

Corollaire :

Si a => b et b => ¬a alors a = faux

Le symbole ¬ est la négation: b => ¬a  signifie b implique “non a”; si b est vrai, alors “¬a” est vrai, donc a est faux.

Pour travailler le corollaire, après avoir démontré que a => b, on doit donc démontrer que b => ¬a. En mettant le booléen b à vrai, on découvre que le booléen a finit par devenir faux. Si c’est le cas, on peut remplacer tous les booléens a dans les grilles par des signes faux.

Comment est effectuée l’implication sur Actilud

Pour que les énigmes ne soit pas trop difficiles, l’implication ne poursuit pas ses déductions jusqu’à la fin de l’énigme. Lorsque le solveur applique la technique de l’implication, il change la valeur d’un booléen, puis il lance les répercussions et fusions,  les intersections, l’autocomplétion (détection des cases qui sont vraies ou fausses en fonction des signes vrai et faux présents). C’est déjà bien suffisant pour détecter des cases intéressantes. Le solveur effectue chacune de ces techniques une seule fois seulement, puis il observe le résultat.