12
$\begingroup$

I've seen how XOR-3-SAT is efficiently solvable (for instance, see the "XOR-satisfiability" section in the Wikipedia entry for Boolean satisfiability problem).

I'm wondering a basic question: Is XOR-k-SAT efficiently solvable, for formulas with varying amounts of literals per clause?

I'd really like to know if we can increase the amounts of literals per clause beyond 3, and if we can have mixed clause lengths.

|cite|improve this question
$\endgroup$
  • 2
    $\begingroup$ What research have you done? We expect you to make a serious effort on your own first, before asking, and to show us in the question what research you've done and what you've tried. Wikipedia mentions that the algorithm for solving XOR-3-SAT is Gaussian elimination. Have you made an attempt to understand how that works, and see whether it applies to XOR-k-SAT? $\endgroup$ – D.W.♦ Apr 13 '15 at 17:17
  • $\begingroup$ @D.W. I admit that I didn't do a lot of research on it. I saw the mention of Gaussian elimination, and figured that this would work for generalized XOR-SAT. But I guess I was looking for confirmation. I hope you will forgive my laziness. I will try to do more research in the future, before asking questions like this. $\endgroup$ – Matt Groff Apr 13 '15 at 17:42
11
$\begingroup$

It looks like the Wikipedia article you linked to says that XORSAT (not just 3-XORSAT) is in P. The method by which they are solving that 3-XORSAT formula in their example very easily generalizes to formulas in which the clauses can have arbitrarily large numbers of variables and differing numbers of variables.

You just look at the formula as a system of linear equations where you have an equation for each clause, and a variable for each variable. For example, the formula:

$$(x_1\oplus x_2\oplus\lnot x_3\oplus x_5)\land (x_2\oplus x_3)$$

has a satisfying assignment if and only if the following system of equations has a solution:

$$x_1+x_2+(1+x_3)+x_5\equiv 1 \mod 2$$ $$x_2+x_3\equiv 1 \mod 2$$

And we can find solutions to linear systems of equations like these in polynomial time using Gaussian elimination!

|cite|improve this answer
$\endgroup$
6
$\begingroup$

Yes. It is solvable by Gaussian elimination. Gaussian elimination can solve any system of equations that is linear modulo. XOR acts as addition modulo 2, so each XOR-SAT clause acts as a linear equation modulo 2. Consequently, Gaussian elimination can solve any XOR-k-SAT formula or any XOR-SAT formula, even if there are a varying number of literals per clause or mixed clause lengths, in polynomial time.

|cite|improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.