Lets imagine we have a satisfiable formula F(A0, A1,...Ak,S0,...,Sn). The problem to solve is "Is there an assignment for variables S0,...,Sn which will make F unsatisfiable?". One way of solving is to find all solutions for F in terms of variables S0,...,Sn and if the count is < 2^n, the missing solution will be the answer, but the complexity of this algorithm is huge, if the number of such assignments is small.
 
My questions are:

 - Is there a way to solve the problem with less SAT solver calls? 
 - Is it a well-known problem in theory (What I should google to read about it)?