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

1 Answer 1

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

$\endgroup$
2
  • $\begingroup$ I had good reasons to doubt my claim. Great counter-example. $\endgroup$
    – user102180
    May 8, 2020 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$
    – user102180
    May 8, 2020 at 21:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.