Vector - gromas/polysat GitHub Wiki

Вектором частичного назначения переменных сочетания трёх переменных из n в рамках исследуемых алгоритмов называется такой вектор {x1,x2,x3...xn} в котором изначальное назначение переменных сочетания (например {x1,x2,x3}) соответствует одному из восьми возможных вариантов назначения трёх переменных из множества {0,1}.

• В результате дальнейшего исследования взаимосвязей между векторами сочетаний решения и процедуры распространения назначений переменных, вектор может назначать себе значения других переменных решения, соответствующие ограничениям, связанным с данным конкретным вектором. Например, если существует один единственный вектор сочетания {x1,x2,x3} и совместимый с ним один единственный вектор сочетания {x1,x2,x4}, то оба этих вектора могут быть расширены до полного соответствия друг другу, любой из них будет назначать все переменные группового набора {x1,x2,x3,x4}.
• Для хранения векторов назначений переменных в решении используется побитное отражение всех переменных задачи на переменные типа ulong (unsigned int64) в массивы bitSet0 и bitSet1, соответствующие биты которых, установленные в значение 1 указывают на назначение переменной значения 0 или значения 1 соответственно.
• В ранней версии решений использовался массив назначений битов data и маска mask, указывающие на соответствующее значение устанавливаемого вектором бита и сам факт установки такого бита, соответствующий битам маски, установленным в единицу.