1
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ I had good reasons to doubt my claim. Great counter-example. $\endgroup$ – d3m4nz3 May 8 at 20:32
  • $\begingroup$ I was so blind, one can easily see it even in 3SAT. If I build a truth table of 3 variables, such that 7 clauses eliminate 7 rows out of 8 and remove any of the 4 clauses that contain more than true 1 literal, new solutions appear. $\endgroup$ – d3m4nz3 May 8 at 21:43

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.