Какой алгоритм решить систему уравнений, в которой переменные - биты, а операция - xor?

Вы можете использовать для этого метод исключения Гаусса: https://en.wikipedia.org/wiki/Gaussian_elimination

XOR - это сложение (и вычитание - то же самое) для целых чисел, взятых по модулю 2, так что это довольно просто:

Найдите, например, уравнение, содержащее v1, и добавьте его ко всем другим уравнениям, содержащим v1, чтобы удалить из них v1:

v1 XOR v2        = 1
      +
v1        XOR v3 = 0
--------------------
       v2 XOR v3 = 1

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

Я почти вставил это в другой комментарий, но это похоже на ответ, так что вот он.

Боюсь, вы можете быть СОЛОМ. Например, при Sx, равном 111, одна ведущая матрица

L1 = 100   | Sx(L1) = 1
L2 = 010   | Sx(l2) = 1
L3 = 001   | Sx(L3) = 1

и есть еще две эквивалентные матрицы, которые подходят для решения (L3 может быть 010 или 100 так же легко).

Кроме того, учитывая Sx, равное 001, вы не будете знать, какой Vx в L3 является «активным» битом, даже если вы знаете, что L1 и L2 имеют коэффициенты 0 для каждой переменной.

Хорошо, для этого вам нужно знать несколько алгебраических правил о xor и not, 0 = false и 1 = true.

Прежде всего, xor удовлетворяет как ассоциативным, так и коммутативным законам. Если мы вместе составим длинную цепочку, мы сможем перестроить все, что душе угодно.

Далее x xor x = 0. Когда мы добавляем к этому тот факт, что 0 xor y = y, мы можем просто отбросить согласованные пары переменных.

Далее подмена. Уравнение вида x1 xor x2 xor ... xor xn = 0 означает, что x1 = x2 xor x3 xor ... xor xn. Аналогичным образом x1 xor x2 xor ... xor xn = 1 означает, что x1 = 1 xor x2 xor x3 xor ... xor xn. Эти факты можно подставить в другие уравнения. Это может привести к повторению переменных, которые мы затем можем отбросить.

Это означает, что каждое уравнение можно использовать для записи одной переменной в терминах других, а затем это можно будет подставить в другие уравнения. Теперь это зависимая переменная. В конце у нас будет одно из трех состояний.

1. 1 = 0 означает, что решений нет.
2. Не осталось ни уравнений, ни переменных. Есть одно решение. Просто замените в обратном порядке, и все готово.
3. Некоторые переменные никогда не исключались, но вы не участвуете в уравнениях. Эти переменные бесплатны. Вы можете настроить их на что угодно и получить ответ. Вы также можете установить их на 1.

Позвольте мне проиллюстрировать ваши уравнения.

(1) 1 = V1 xor V2 xor V3
(2) 0 = V1 xor V2
(3) 1 = V2 xor V3

Из (1) мы знаем, что:

(4) V1 = 1 xor V2 xor V3

(Обратите внимание, V1 исключено.) Подставьте (4) на (2) и (3), чтобы получить:

(5) 0 = V1 xor V2
      = (1 xor V2 xor V3) xor V2
      = 1 xor V3

(6) 1 = V2 xor V3

(Обратите внимание, что (6) - тривиальная замена.)

От (5) получаем:

(7) 1 = V3

(Обратите внимание, V3 исключено.) Подставляем (7) в (6), и мы получаем:

(8) 1 = V2 xor V3
      = V2 xor 1

От (8) получаем:

(9) V2 = 1 xor 1 = 0

(Примечание: V2 исключено.)

Правила (9), (7) и (4) исключили V2, V3 и V1, так что есть одно решение. И это:

(9) V2 = 0
(7) V3 = 1
(4) V1 = 1 xor V2 xor V3 = 1 xor 0 xor 1 = 0

Обратите внимание, что это полностью механическая процедура. На каждом этапе я брал первое оставшееся уравнение, использовал его, чтобы записать одну переменную через другие, а затем подставлял его в другие. На одно уравнение меньше, на одну переменную меньше. Это всегда срабатывает.

Для этого вам нужно будет разработать хорошее представление и код. Но мы надеемся, что знание того, что вы пытаетесь сделать, поможет.

Вы можете использовать алгоритм MiniSAT. Например, в Java он доступен в проекте LogicNG.

Ваш пример можно опубликовать следующим образом в SatisfiabilityInstances () функция проекта Symja. Под капотом LogicNG MiniSat.miniSat () называется.

SatisfiabilityInstances(Xor(v1,v2,v3)&&Not(Xor(v1,v2))&&Xor(v2,v3),{v1,v2,v3})

результат:

{{False,False,True}}