Какой алгоритм для решения системы уравнений, где переменные являются битами, а операция - xor? - PullRequest
1 голос
/ 24 апреля 2019

Я пытаюсь решить систему уравнений. Каждое уравнение имеет вид:

V1 xor V2 xor ... xor Vx = Sx

Vx и Sx - это одноразрядные переменные. Sx известны, и мне нужно найти значение всех Vx


например:

V1 xor V2 xor V3 = 1
V1 xor V2 = 0
V2 xor V3 = 1

(решение V1 = 0, V2 = 0, V3 = 1)


На самом деле у меня есть тысячи переменных (каждая - один бит) и тысячи уравнений (только операции xor). Я знаю, что есть хотя бы одно решение, и мне нужно только одно решение.

Я знаю, как решить это вручную для небольшой системы, но я не знаю, как создать алгоритм для решения этой проблемы.

Можете ли вы помочь мне с этим? Я разработчик и понимаю, как работать с битами, операторами xor и структурами данных, но у меня меньше опыта в математике, и я не знаю, какой метод решения системы уравнений использовать. Я также не очень интуитивно с матричными операциями, поэтому, если мне это нужно, попробуйте объяснить это очень медленно! : Р

Спасибо!

Ответы [ 4 ]

4 голосов
/ 24 апреля 2019

Для этого можно использовать исключение Гаусса: 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 и т. Д., Пока все уравнения не будут иметь только одну переменную.

0 голосов
/ 29 апреля 2019

Вы можете использовать алгоритм 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}}
0 голосов
/ 24 апреля 2019

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

Прежде всего, xor удовлетворяет как ассоциативному, так и коммутативному законам. Если мы 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

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

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

0 голосов
/ 24 апреля 2019

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

Боюсь, вы можете быть SOL.Например, при Sx, равном 111, одна матрица, идущая впереди, имеет значение

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

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

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

...