Unique 1-in-3 SAT

Question

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

I know the value of each bit of the unique assignment because 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 A and B in correct order in the input bits.

The number of true literals in each clause is either 1, 2 or 3. Because I know the value of each bit, I can tell exactly which literals are true in each clause, and count them. For example, I know which clauses are satisfied by exactly 1 literal. And that literal is logically part of the unique solution.

My question is simple: If I remove all the clauses with more than 1 true literal, will the assignment necessarily still be unique?

In other words, if I wanted to write down a resolution proof (likely exponentially long) to demonstrate that the solution is unique (Another Solution Problem, in Co-NP), can I write it down using only the clauses with 1 true literal?

Intuitively, I think so, but I am unable to defend my point of view, even when thinking about the 2SAT equivalent.

Answer 1

Consider the following CNF: $$ (a \lor \lnot b) \land (\lnot a \lor b) \land (a \lor b). $$ It has a unique satisfying assignment, $a=b=\top$, which satisfies the last clause twice. However, if you remove the last clause, then you get another satisfying assignment, $a=b=\bot$.