Exactly $1$-in-$3$ SAT ($X_3SAT$) is a variant of the Boolean satisfiability problem. Given a set of clauses, each clause having three literals, is there a set of literals such that each clause contains exactly one literal from this set?

$X_3SAT$ is known to be $NP$-complete. It remains $NP$-Complete even when it is monotone (all literals are positive) and linear (no two clauses share more than one variable in common).

I think an unsatisfiable monotone linear instance must have at least four loops. A loop is a sequence of clauses such that each clause has one variable in common with the previous clause in the sequence, a different variable in common with the next clause, and no variables in common with any other clauses in the sequence. The last clause in the sequence "loops" around to the first. Loops have relatively few satisfying assignments. A monotone linear length three loop has four satisfying assignments. Loops can often be reduced and removed. These are some reduction rules for loops.

X() = $X_3SAT$ instance

($a,b,c$) = $X_3SAT$ clause (choose exactly one literal to be True)

X($T \leftarrow a$) = replace literal $a$ with True and $\overline{a}$ with False

X($a \leftarrow \overline{b}$) = replace literal $\overline{b}$ with $a$ and $b$ with $\overline{a}$

Some Loop Reduction Rules:

$(x_1,y_1,y_2)(x_2,y_2,y_3)(x_3, \overline{y_3}, \overline{y_1}) + X() = (x_1,x_2,x_3) + X(F \leftarrow y_2,x_1 \leftarrow \overline{y_1},x_2 \leftarrow \overline{y_3})$

$(x_1,y_1,y_2)(x_2,y_2,y_3)(x_3,y_3,y_1)(x_1,x_2,z_1) + X() = (x_1,x_2,x_3) + X(x_1 \leftarrow y_3,x_2 \leftarrow y_1,x_3 \leftarrow y_2,x_3 \leftarrow z_1)$

$(x_1,y_1,y_2)(x_2,y_2,y_3)(x_3,y_3,y_1)(x_1,y_3,z_1) + X() = (x_1, \overline{x_2}, \overline{x_3}) + X(F \leftarrow y_3,x_2 \leftarrow \overline{y_2},x_3 \leftarrow \overline{y_1},x_1 \leftarrow \overline{z_1})$

$(x_1,y_1,y_2)(x_2,y_2,y_3)(x_3,y_3,y_4)(x_4,y_4,y_1)(x_1,x_2,x_3) + X() = X(F \leftarrow x_2,T \leftarrow x_4,F \leftarrow y_1,F \leftarrow y_4,x1 \leftarrow \overline{x_3},x1 \leftarrow \overline{y_2},x1 \leftarrow y_3)$

$(x_1,y_1,y_2)(x_2, \overline{y_2}, \overline{y_3}) + ... + (x_{k-1},y_{k-1},y_k)(x_k, \overline{y_k}, \overline{y_1}) + X() = X(F \leftarrow x_1,F \leftarrow x_2,...,F \leftarrow \overline{x_{k-1}},F \leftarrow x_k,y_1 \leftarrow \overline{y_2},...,y_1 \leftarrow y_{k-1},y_1 \leftarrow \overline{y_k})$ for k even

$(x1, \overline{y_1},y_2)(x_2, \overline{y_2},y_3) + ... + (x_k, \overline{y_k},y_1) + X() = X(F \leftarrow x_1,F \leftarrow x_2,...,F \leftarrow x_k,y_1 \leftarrow y_2,y_1 \leftarrow y_3,...,y_1 \leftarrow y_k)$

I am looking for other loop reductions.

  • $\begingroup$ Your definition of loops does not match your loops. For example in the second reduction, y1 is both in the 1st and 3rd clause, which does not satisfy that a clause does does not have any variable in common with any other clause (other than the previous and next). Exactly the same also happens in the first reduction. $\endgroup$ Commented Jan 1, 2018 at 20:58
  • 1
    $\begingroup$ The second example is a length three loop with an additional clause. Only the first three clauses are in the loop. This length three loop isn't reducible by itself, but adding the clause $(x_1,x_2,z_1)$ allows the loop to be reduced. Also, the first and last clauses in the loop are assumed to be connected. $\endgroup$ Commented Jan 2, 2018 at 0:34
  • $\begingroup$ Your reductions are still problematic. For example the first one, suppose beforehand, $X() = (x_1,-x_2,-x_2)$. Then the total formula is not satisfiable. After the reduction, $(x_1,x_2,x_3)(-y_1,y_3,y_3)$ is satisfiable $\endgroup$ Commented Jan 2, 2018 at 11:50
  • 1
    $\begingroup$ The conversion is to replace $-y_1$ with $x_1$. If we reverse the conversion, $X(y1 \leftarrow -x1, y3 \leftarrow -x2)$, then $(x_1,x_2,x_3)(-y_1,y_3,y_3)$ becomes $(-y_1,-y_3,x_3)(-y_1,y_3,y_3)$ which is unsatisfiable. $\endgroup$ Commented Jan 3, 2018 at 3:59


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.