Lets imagine we have a satisfiable formula $F(A_0, A_1,...A_k,S_0,...,S_n)$ The problem to solve is Is there an assignment for variables $(S_0,...,S_n)$ which will make F unsatisfiable?. One way of solving is to find all solutions for F in terms of variables $S_0,...,S_n$ 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)?
Assignment to make formula unsatisfiable
logic;satisfiability;sat solvers
Your problem is the canonical $\Sigma_2^P$-complete problem:$$\exists \vec{S} \forall \vec{A} \lnot F(\vec{A},\vec{S}).$$As such, it is thought to be more difficult than SAT (which is $\Sigma_1^P$). Solving it with a few SAT-oracle calls is akin to solving SAT itself efficiently (the P vs. NP question), though it could be that $\Sigma_2^P = \Sigma_1^P$ while $P \neq NP$, so in some sense there is more hope for your problem than for SAT itself.