# Is it possible to remove exactly one solution from a CNF in polynomial time?

Given a conjunctive normal form (CNF) is it possible to remove one solution from its set of solutions (irrespective of whether the CNF has a solution or not in the first place)? By that I am asking if there is a new formula that will reduce the number of solutions of the original by one i.e. if the original one has 0 solutions then the newly constructed one will have 0 as well but if the original one has x solutions (x > 0) then the new one will have x-1.
If not (this might be in NP) is there an easy way to find a bound on the number of solutions removed?

Forcing a variable to take a specific value has the inconvenience of perhaps resulting in no solution at all (it might be the case that there is only one solution to begin with but it might also be the case where the N solutions depended on the variable taking another specific value).

For instance: e.g. Given (x1 V x2)^(!x1 V x2) - a CNF with possible solutions: x1 = T, x2 = T and x1=F, x2=T, I would like to construct a CNF with solution x1 = T, x2 = T only (or x1=F, x2=T only). (Note: ! = not and V = or)

-
Clearly it's not possible to remove exactly one solution from the solution set irrespective (not "disrespective") of whether there is a solution or not, since if there's no solution no solution can be removed. – joriki Nov 16 '11 at 4:47
I think that the essential part of this question is interesting, but I agree with joriki that in its current form, the answer is “no” for a trivial and inessential reason. – Tsuyoshi Ito Nov 17 '11 at 21:27
You're right I wasn't as precise as I should have been. I fixed this hopefully. – William Nov 19 '11 at 18:49