Является ли обобщенный XOR-SAT эффективно разрешимым?

12

Я видел, как XOR-3-SAT эффективно разрешима (например, см. Раздел «XOR-удовлетворяемость» в статье Википедии для проблемы булевой выполнимости ).

Мне интересно основной вопрос: эффективно ли разрешим XOR-k-SAT для формул с различным количеством литералов в предложении?

Мне бы очень хотелось узнать, сможем ли мы увеличить количество литералов в предложении выше 3, и можем ли мы иметь смешанные длины предложений.

complexity-theory satisfiability Мэтт Грофф
источник
2
Какие исследования вы провели? Мы ожидаем, что вы сначала приложите серьезные усилия, прежде чем спросить, и покажете нам в вопросе, какие исследования вы провели и что вы пробовали. В Википедии упоминается, что алгоритм решения XOR-3-SAT - это исключение Гаусса. Вы пытались понять, как это работает, и посмотреть, применимо ли это к XOR-k-SAT?
DW
@ DW Я признаю, что я не проводил много исследований по этому вопросу. Я видел упоминание об исключении Гаусса и полагал, что это будет работать для обобщенного XOR-SAT. Но я думаю, я искал подтверждение. Я надеюсь, вы простите мою лень. Я постараюсь сделать больше исследований в будущем, прежде чем задавать подобные вопросы.
Мэтт Грофф

Ответы:

11

Похоже, что статья в Википедии, на которую вы ссылаетесь, говорит, что XORSAT (не только 3-XORSAT) находится в P. Метод, с помощью которого они решают эту формулу 3-XORSAT в своем примере, очень легко обобщает формулы, в которых предложения могут иметь произвольно большое количество переменных и различное количество переменных.

Вы просто смотрите на формулу как систему линейных уравнений, где у вас есть уравнение для каждого предложения и переменная для каждой переменной. Например, формула:

(x1⊕x2⊕¬x3⊕x5)∧(x2⊕x3)

имеет удовлетворительное назначение тогда и только тогда, когда решение имеет следующая система уравнений:

x1+x2+(1+x3)+x5≡1mod2
x2+x3≡1mod2

И мы можем найти решения таких линейных систем уравнений за полиномиальное время, используя исключение Гаусса!

Дилан Маккей
источник
6

Да. Это разрешимо устранением Гаусса. Устранение Гаусса может решить любую систему уравнений, которая является линейной по модулю. XOR действует как сложение по модулю 2, поэтому каждое предложение XOR-SAT действует как линейное уравнение по модулю 2. Следовательно, удаление по Гауссу может решить любую формулу XOR-k-SAT или любую формулу XOR-SAT, даже если существует различное количество литералов по длине предложения или по смешанному предложению, за полиномиальное время.

DW
источник