# Assignment to make formula unsatisfiable

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?
• "which will make F unsatisfiable" -- that does not make sense. Do you simply mean "does not satisfy F"? Then you are talking about the problem TAUTOLOGY (resp. it's complement). – Raphael May 29 '15 at 15:26
• Ignoring the fact that the question doesn't make sense, I think trying to find a solution to $\neg F(A_0,A_1,\ldots, A_k,S_0,\ldots, S_n)$ might be what you are looking for. – Dave Clarke May 29 '15 at 15:34
• Maybe I wasn't clear. After applying assignments for $(S_0,...,S_n)$ we will have another formula $G(A_0 ,..., A_k)$ and this must be unsatisfiable. – Grigor Aghanyan May 29 '15 at 15:36

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.
• Exactly. Thank you for the answer. So the solution with $2^n$ solver calls is "not a bad solution" for it? Some link for papers about this problem will help me lot. – Grigor Aghanyan May 29 '15 at 15:58
• Practically speaking there could be heuristics that work well for some problems, but I'm unaware of any. The polynomial hierarchy (which contains $\Sigma_2^P$) should be covered in any textbook on computational complexity. – Yuval Filmus May 29 '15 at 16:00