Я иногда очень удивляюсь

[thesz]

https://arxiv.org/pdf/1508.05117 - страница 8, правый столбец.

"∂+i (resp. ∂-i) is the set of clauses satisfied by setting xi = 1 (resp. xi = −1

Comments

[p2004r]

Переменные, освобожденные через backtrack(), фактически не "возвращаются в алгоритм распространения оценок" в полном смысле слова. Их восстановление выглядит как простое снятие фиксации без явной переоценки на уровне SP-сообщений.
Нет случайного выбора значений: Код не использует случайные значения для освобожденных переменных.

[thesz]

В статье они говорили, что периодически выполняется переоценка для выбранных переменных (перевычисляется bias). Но в коде может быть что угодно, в моих прогонах он совершенно не делал отката, например.