На странице википедии здесь довольно хорошо описан алгоритм CDCL (и, похоже, фотографии были взяты из слайдов, созданных Шарадом Маликом в Принстоне). Тем не менее, при описании того, как откатить все, что он говорит, это «до соответствующей точки». MiniSAT также использует вариант алгоритма CDCL, поэтому я прочитал эту статью, Похоже, они говорят, что вы должны вернуться, пока выученное предложение не станет единичным предложением. Это, конечно, разъяснение, но это не имеет смысла для меня. Насколько я могу судить, последнее назначение определенно будет частью оговорки изученного конфликта (возможно, я здесь не прав?), Поэтому, когда вы вернетесь на один шаг назад, вы сразу же сделаете единицу изученного предложения, последнее присвоенное значение будет отображаться, и алгоритм будет работать точно так же, как и DPLL, и не будет проходить достаточно далеко. Кроме того, страница википедии не следует этому правилу, она отступает намного дальше, как кажется желательным.
Как далеко можно вернуться?