8
$\begingroup$

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)?
Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ "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). $\endgroup$
    – Raphael
    Commented May 29, 2015 at 15:26
  • $\begingroup$ 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. $\endgroup$
    – Dave Clarke
    Commented May 29, 2015 at 15:34
  • $\begingroup$ 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. $\endgroup$
    – Grigor Aghanyan
    Commented May 29, 2015 at 15:36

2 Answers 2

Reset to default
6
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Grigor Aghanyan
    Commented May 29, 2015 at 15:58
  • $\begingroup$ 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. $\endgroup$
    – Yuval Filmus
    Commented May 29, 2015 at 16:00
4
$\begingroup$

This is a well-known problem: it is the 2QBF problem. Unfortunately, it's significantly harder than SAT. There are QBF solvers available. You could try finding a QBF solver (or, even better yet, a 2QBF solver) and seeing if it can solve your formula. However, QBF solvers don't scale as well as SAT solvers; QBF is significantly harder than SAT.

See https://cstheory.stackexchange.com/q/11022/5038 and http://www.qbflib.org/ for some resources that might be helpful.

Improve this answer
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.