En la página de Wikipedia aquí , describe bastante bien el algoritmo CDCL (y parece que las imágenes fueron tomadas de diapositivas creadas por Sharad Malik en Princeton). Sin embargo, al describir cómo dar marcha atrás, todo lo que dice es "al punto apropiado". MiniSAT también usa una variante del algoritmo CDCL, así que leí este artículo. Lo que parecen decir es que debes retroceder hasta que la cláusula aprendida sea una cláusula de unidad. Eso es sin duda una aclaración, pero no tiene sentido para mí. La última asignación definitivamente será parte de la cláusula de conflicto aprendido hasta donde puedo decir (¿tal vez estoy equivocado aquí?) Entonces, cuando retrocedas un paso, inmediatamente harás la unidad de cláusula aprendida, el último valor asignado cambiará, y el algoritmo procederá exactamente como DPLL sin tener que retroceder lo suficiente. Además, la página de Wikipedia no sigue esta regla, retrocede mucho más como parece deseable.
¿Hasta dónde se supone que uno debe retroceder?