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.