Linear satisfability - gromas/polysat GitHub Wiki

Под линейной выполнимостью я подразумеваю такую последовательность действий, которая позволяет выявить линейно-невыполнимые назначения и эффективно удалить их из рассматриваемого решения. Для решения данной задачи рассмотрим взаимосвязи векторов назначений в каждом сочетании, приводящие к невозможности выполнения условия задачи k-SAT, а именно - к невозможности полного назначения всех переменных.

• (1) Если в каком-то сочетании из трёх переменных не существует ни одного вектора частичных назначений, это ведет к невозможности назначить этим переменным какие-либо значения. Указанный факт является основным при поиске условия невыполнимости задачи. При обнаружении данного факта задача считается разрешенной с резолюцией UNSATisfable.
• (2) Если для вектора частичных назначений не существует хотя бы одного совместимого с ним вектора в каждом из сочетаний, то для данного вектора ни при каких условиях невозможно полностью назначить все переменные решения. При обнаружении такого вектора, он удаляется из списка векторов сочетания. Если удаляемый вектор был последним в сочетании, то необходимо воспользоваться правилом (1) с резолюцией UNSATisfable.