Верблюд,


Вот смотрите, актуализация одной из переменных в 1 или 0 даёт две функции, каждую из которых надо решать.
Если допустить, что функция решаема, тут два решения: либо сразу выяснится, что 1 из них несовместима, либо в обоих случаях конфликта не будет
Допустим, вы прошлись по всем переменным и попробовали произвести такую замену
и оказывается, что конфликтов нет

ваши действия?

Верблюд,

я вам простой пример приведу
допустим есть число
n = P1 * P2 - произведение двух простых

если я запишу в 3-кнф функцию описывающую уравнение
n mod a = 0

оно естественно будет иметь два решения 1 и P2 (я ограничу количество бит корнем из n)

соответственно лишь часть P2 будет иметь нулевые биты (а может и вообще не иметь)
для остальных переменных будет 1
и как вы не задавайте у вас для любой разбивки будут оба решения

Верблюд,

вот кстати
задавать значение переменным сложнее, чем выставлять равенство\неравенство переменных

т.е., если функция содержит два включения
(vi, vj, p1) и (vi, vj, p2)
и если при задании p1=p2 или p1 = not p2 выявится конфликт, то мы выразим одну переменную через другую

так же по аналогии с алгоритмом Карацубы
для (vi, pa, pb) и (vi, pc, pd) разрешение конфликтов подобным образом может дать 3 ветвления за 2 замены, а не 4


В литературе ещё есть разбиения функции на две независимых функции, у вас этот вопрос как-то вообще упущен.

Верблюд,

ещё такая мысль: если алгоритм будет доказанно "стопориться" только при наличии нетривиальных решений, то такой алгоритм уже приобретёт ценность

Верблюд,

опять в том же ракурсе, сложно понять это, и доказательности мало, речь вообще очень тяжело воспринимается

хотя какая-то аналогия идёт с заменой переменных для перевода в 2-КНФ

[spoiler] [quote=Верблюд]Короткое видео о том откуда появился алгоритм.