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)