Vector compatibility - gromas/polysat GitHub Wiki

Два вектора неполных назначений переменных считаются совместимыми друг с другом, если назначаемые ими значения переменных не противоречат друг другу.

• Совместимость векторов частичных назначений различных сочетаний определяется путем побитного сравнения устанавливаемых ими значений переменных. При отсутствии противоречивых назначений такие два вектора считаются совместимыми друг с другом. Например, если существует вектор назначений сочетания {x1,x2,x3}, устанавливающий переменные сочетания в 010, и существует вектор сочетания {x3,x4,x5}, устанавливающий переменные сочетания в 000, то такие векторы будут совместимы, так как пересечение множеств назначений этих векторов {x3} не противоречит друг другу {0}.
• Условие непротиворечивости касается так же всех назначений переменных, добавленных к вектору в результате работы процедуры распространения назначений переменных.