Clause pilotée par les conflits Apprentissage de la clarification du retour en arrière

Sur la page wikipedia ici, il décrit assez bien l'algorithme CDCL (et il semble que les photos ont été prises à partir de diapositives créées par Sharad Malik à Princeton). Cependant, quand il décrit comment revenir en arrière, tout ce qu'il dit est "au point approprié". MiniSAT utilise également une variante de l'algorithme CDCL, j'ai donc lu ce document. Ce qu'ils semblent dire, c'est que vous devriez revenir en arrière jusqu'à ce que la clause apprise soit une clause unitaire. C'est certainement une clarification, mais cela n'a pas de sens pour moi. La dernière affectation va certainement faire partie de la clause de conflit apprise pour autant que je sache (peut-être que je me trompe ici?) Donc lorsque vous revenez en arrière d'une étape, vous ferez immédiatement l'unité de la clause apprise, la dernière valeur affectée sera inversée, et l'algorithme se déroulera exactement comme DPLL sans jamais revenir en arrière suffisamment loin. De plus, la page wikipedia ne suit pas cette règle, elle revient beaucoup plus loin comme cela semble souhaitable.

Jusqu'où doit-on revenir en arrière?

Voici le paragraphe pertinent du document MiniSAT:

$False$

Un point que vous semblez avoir manqué est qu'une fois que la clause apprise devient l'unité en raison d'affectations annulées (retour en arrière), le solveur ne s'arrête pas là. Il pourrait y avoir d'autres affectations avant celle-ci qui n'ont aucune incidence sur le conflit actuel et expérimentalement, il a été démontré qu'il vaut mieux annuler ces affectations non liées également. Ainsi, le solveur continue d'annuler les affectations jusqu'à ce que la prochaine annulation rende la clause apprise non unitaire, c'est-à-dire qu'elle contiendrait plus d'une variable non affectée. Le solveur s'arrête ici, exécute la propagation d'unité pour satisfaire la clause d'unité, puis reprend la recherche, en affectant des variables normalement.

Notez également que la variable de décision actuelle peut ne pas être présente dans la clause apprise. Une stratégie courante pour un solveur CDCL consiste à trouver le premier point d'implication unique et à utiliser cette variable dans la clause apprise. Dans certains cas, le premier UIP est la variable de décision, mais ce n'est souvent pas le cas.