patternMinor
Assignment to make formula unsatisfiable
Viewed 0 times
unsatisfiableassignmentmakeformula
Problem
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
- Is it a well-known problem in theory (What I should google to read about it)?
Solution
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.
$$
\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.
Context
StackExchange Computer Science Q#43074, answer score: 6
Revisions (0)
No revisions yet.