Unique 3SAT to Unique 1-in-3SAT

Question

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?

Answer 1

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$.

Answer 2

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).