Combination - gromas/polysat GitHub Wiki

Алгоритм работает с сочетаниями трёх переменных из n, содержащими по восемь векторов частичных назначений, соответствующих восьми различным назначениям этих трёх переменных: {000, 001, 010, 011, 100, 101, 110, 111}.

• Каждый элементарный дизъюнкт исследуемой формулы 3-КНФ, переменные литералов которого соответствуют сочетанию, отражается в область векторов данного сочетания через удаление соответствующего ему вектора назначения переменных сочетания. Например, если для сочетания переменных {x1, x2, x3} в исходной формуле существует элементарный дизъюнкт {x1, x2, !x3}, из списка векторов назначений сочетания удаляется вектор назначения 001.
• Первоначальный вариант алгоритма использовал все возможные сочетания по три переменных из n. Всего существует (n^3-3n^2+2n)/6 вариантов таких сочетаний. Данный вариант оказался избыточным и в дальнейшем сочетания, содержащие все восемь возможных векторов сочетаний были исключены из рассмотрения, так как они не влияют на решение задачи.