Suppose I have a CNF formula with clauses of size 2 and 3. It has a unique satisfying assignment.

It was made from a binary multiplication circuit where I multiplied two primes numbers A and B such that A*B=S where S is a semiprime number. I added the conditions that A != 1, B != 1 and A <= B, then added the value of S to the formula make sure the assignment is unique. The only way to satisfy the formula is to put the values of primes A and B in correct order in the input bits.

In 1-in-3SAT, we force that exactly 1 literal should be true in each triplet and two others false. If exactly 2 literals are true we can flip all the iterals in the clause to get an equivalent 1-in-3SAT clause (in other words 2-in-3SAT is the same problem).

Basic observation: While a regular OR clause eliminates 1 possibility out of 8, a 1-in-3 clause eliminates 5 possibilities out of 8.

3SAT can be reduced to 1-in-3 SAT, such that if the 3SAT formula is satisfiable then so is the reduced formula.

However, reductions do not seem to preserve the number of assignments, by introducing new variables without forcing their value.

Can Unique 3SAT be reduced to Unique 1-in-3SAT...

  1. Without knowing the correct assignment?
  2. If not, while knowing the correct assignment?
  • $\begingroup$ No, by '<=' I was reffering to the arithmetic comparison operator. It doesn't take length into account. You can implement this with a serie of OR, AND and NOT, basically one boolean operation to compare each bit. The result is a bit which says if A <= B or not. Then you add a unit clause which says this bit has to be true. If you use 67 and 71, then 67 has to be A and 71 has to be B, otherwise the formula is not satisfied. $\endgroup$
    – d3m4nz3
    May 9, 2020 at 20:21

2 Answers 2


Yes, a 3-SAT formula $\phi$ can be transformed into a 1-in-3 SAT formula $\phi'$ while preserving the number of satisfying assignments. To avoid ambiguities I will use "$\vee$" between literals of a 3-SAT clause, and commas between literals of a 1-in-3 SAT clause.

Let me preliminarily show that, given two literals $a$ and $b$, we can simulate a new type of clause $(x = a \wedge b)$ that forces the value of a new variable $x$ to be $a \wedge b$ using only 1-in-3 SAT constraints, without introducing any new solution.

Consider the cluases: $$ (\overline{b}, c, x) \wedge (a, c, d) \wedge (\overline{a}, e, x) \wedge (b, e, f) $$

If $a=\top$, and $b=\top$, then the 2nd and 4th clauses ensures that $c=d=e=f=\bot$. The 1st and 3rd clauses then ensures that $x=\top$.

If $a=\top$, and $b=\bot$, then the 2nd clause ensures that $c=d=\bot$. The 1st clause then ensures that $x=\bot$. The 3rd clause ensures that $e=\top$, and the 4th clause implies $f=\bot$.

The case $a=\bot$, and $b=\top$ is symmetric.

If $a=\bot$ and $b=\bot$, then the 1st and 3rd clauses imply $c=e=x=\bot$. The 2nd and 4th clauses ensure $d=f=\top$.

I am now ready to transform a formula $\phi$ of 3SAT to a formula $\phi'$ of 1-in-3 SAT. Consider now a clause $(a \vee b \vee c)$ of $\phi$. This can be transformed into the following equivalent 1-in-3 SAT clauses:

  • Add a new variable $x$ that is true iff $a$ is false and $b$ is true. This is encoded by the clause $(x = \overline{a} \wedge b)$.

  • Add a new variable $y$ that is true iff $a$ is false, $b$ is false, and $c$ is true. We will need an additional variable $z$. The clause $(z = \overline{a} \wedge \overline{b})$ ensures that $z$ is true if and only if $a$ is false and $b$ is false. Then, the value of $y$ can be enforced by the clause $(y = z \wedge c)$.

  • If $(a \vee b \vee c)$ is true then at least one of $a$, $b$, or $c$ is true. This means that exactly one of $a$, $x$, and $y$ is true. On the converse, if $(a \vee b \vee c)$ is false, then at all of $a$, $x$, and $y$ are false. This shows that $(a \vee b \vee c)$ is satisfiable if and only if $(a, x, y$) is satisfiable.

We have then constructed an equivalent 1-in-3 SAT formula $\phi'$ that uses a superset of the variables of the original 3 SAT formula $\phi$. A truth assignment to the variables of $\phi'$ satisfies $\phi'$ if and only if the assignment restricted to the variables of $\phi$ satisfies $\phi$. Therefore, if any new solution to $\phi'$ is introduced, it must be because of the newly added variables $x$, $y$, and $z$ (one set for each clause). However, the values of these variables are completely determined by the values of the variables of $\phi$.

  • $\begingroup$ This appears to be valid. Can I easily adapt it for clauses of size 2? I need to get rid of those too, otherwise the problem is mixed between 1-in-3 SAT and 2SAT. Basically, I'm perfectly willing to introduce 1-in-2 clauses but no OR clauses. $\endgroup$
    – d3m4nz3
    May 9, 2020 at 12:02
  • 1
    $\begingroup$ Yes, clauses of size 2 can be handled too by modifying the 3-SAT instance. Add $3$ new variables $x$, $y$, and $z$ and $7$ new clauses that force $x$, $y$, and $z$ to all be false (for every assignment that sets at least one of $x$, $y$, and $z$ to true, add a clause that evaluates to false in that case. E.g, for $x=\top$, $y=\bot$, $z=\top$, add the clause $(\overline{x} \vee y \vee \overline{z})$ ). You can now use $x$, $y$ and $z$ as "padding". If you have the clause $(a \vee b)$ you can replace it by $(a \vee b \vee x)$. $\endgroup$
    – Steven
    May 9, 2020 at 12:09
  • $\begingroup$ Hmm I'm having some doubts when trying to assert the validity of the reduction. Suppose in (a∨b∨c), a is true, b is true, c is false, as part of the unique solution. Now why would (a,b,z) have exactly 1 true literal? $\endgroup$
    – d3m4nz3
    May 9, 2020 at 12:42
  • 1
    $\begingroup$ What about now? :) $\endgroup$
    – Steven
    May 9, 2020 at 14:15
  • 1
    $\begingroup$ I'm impressed by the preliminary claim because 1) I checked all 128 possibilities for a,b,c,d,e,f,x and it is true and does not create new solutions 2) If we can do it with AND then we can do with OR (because !x = !a ∨ !b) 3) If we can do it with OR then we can simulate any CNF formula using it. So I'd say correct without even checking second part. $\endgroup$
    – d3m4nz3
    May 9, 2020 at 14:46

Such a reduction is described in Appendix B of Régis Barbanchon, On unique graph 3-colorability and parsimonious reductions in the plane. Barbanchon attributes it to previous work ([9] in the bibliography). Elsewhere, I have seen an attribution to Schaefer's celebrated paper in which he proves his famous dichotomy theorem, among else giving a reduction from 3SAT to 1-in-3SAT, which is supposedly parsimonious (I haven't checked).


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.