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

3SAT can be reduced to 1-in-3 SAT. In 1-in-3SAT, we force that exactly 1 literal should be true in each triplet and two others false.

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

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

- Without knowing the correct assignment?
- If not, while knowing the correct assignment?