Circular deadlock loop - gromas/polysat GitHub Wiki

Циклическая взаимоблокировка векторов полных назначений переменных является следствием невозможности полного распространения назначений переменных между векторами частичных назначений.

• Проблема циклической взаимоблокировки решается путем исследования решения с исключением всех векторов сочетания, кроме исследуемого. При этом становится невозможным получить полный путь назначений переменных, приводящий в какой-либо другой вектор частичных назначений сочетания кроме исследуемого. Если для исследуемого вектора не существует цепочка частичных назначений, приводящая к замыканию исследуемого вектора самого в себя (не существует совместимых векторов хотя бы в одном сочетании), такой вектор удаляется из решения и в дальнейшем не рассматривается.
• Указанная проблема не существует для задач 2-SAT в силу того, что невозможно сделать импликацию назначения переменной вектора сочетания в два различных других сочетания (в силу того, что в 2-SAT задаче всего два литерала в элементарном дизъюнкте) и как следствие, невозможно создать два пересекающихся потока назначений с арбитром. Под арбитром в данном случае подразумевается набор векторов, пересекающих между собой два потока назначений.
• Например, если для задачи с 4 переменными {x1,x2,x3,x4} в сочетании {x1,x2,x3} существуют векторы {001,010}, в сочетании {x1,x3,x4} существуют векторы {001,010} и в сочетании {x1,x2,x4} существуют векторы {001,010}, то линейный алгоритм обнаружит, что для каждого из векторов существует как минимум один совместимый с ним вектор в каждом сочетании из трёх переменных. Тем не менее, задача не имеет решений, так как приводит к цепочке назначений {x1,x2,x3}={001}=>{x1,x3,x4}={010}=>{x1,x2,x4}={010}=>{x1,x2,x3}={010}=>..., то есть набору переменных {x1,x2,x3} назначается два противоречащих друг друга набора назначений. После исключения из рассмотрения одного из векторов сочетания {x1,x2,x3} будет обнаружено, что для одного из векторов сочетаний {x1,x2,x4} и {x1,x3,x4} не существует совместимого вектора в {x1,x2,x3}, что приведет к их удалению. В результате оставшиеся векторы указанных сочетаний будут противоречить друг другу, что так же приведет к их удалению. Так как это последние векторы в данных сочетаниях, их удаление приведет к невозможности назначить значение переменной x4, что в свою очередь приведет к отсутствию возможных решений с назначениями из исследуемого вектора сочетания {x1,x2,x3}. Вектор будет удален. Исследование оставшихся векторов приведет к отсутствию совместимого вектора в одном из сочетаний и резолюции UNSATisfable.