Алгоритмы случайного поиска решения лучше справляются со случайными задачами логической выполнимости, а алгоритмы с перебором и распространением (DPLL) со структурированными задачами.
(я делал
алгоритм доказательства работы на основе случайной SAT - с 5SAT вблизи фазового перехода ни один из современных структурных решателей справиться не мог, а yalsat щелкал их, как орешки)
Алгоритм удаления переменных через разрешение ограничений делает задачу более случайной, то есть, более подходящей для случайного поиска. Поэтому мне это и интересно.
Ну, и про фазовый переход.
Мы можем создавать КНФ с определённым размером ограничений. Например, 2КНФ это КНФ с длиной ограничений в два присваивания переменных - переменные должны быть разные, само собой, и ограничение не должно быть тавтологией. И ограничения внутри КНФ должны быть разными. 2КНФ могут быть разрешены за полиномиальное время, к слову. 3КНФ это КНФ с длиной ограничений в 3, и так далее.
Так вот, существует интересная зависимость между количеством переменных n, количеством ограничений m и длиной ограничений k - вблизи некоторого значения M=neO(k) вероятность получения КНФ без решения очень быстро возрастает. При m заметно меньше M решение найти просто, при m заметно больше M решения не существует с высокой вероятностью, а вот в районе M вероятность очень быстро меняется.