Skip to main content
Computer Science

Return to Question

Tweeted twitter.com/#!/StackCompSci/status/604430043411062785
added 18 characters in body
Source Link
Grigor Aghanyan
Grigor Aghanyan
  • 83
  • 4

Lets imagine we have a satisfiable formula F(A0, A1,...Ak,S0,...,Sn).$F(A_0, A_1,...A_k,S_0,...,S_n)$ The problem to solve is "Is there an assignment for variables S0,...,Sn$(S_0,...,S_n)$ which will make F unsatisfiable?". One way of solving is to find all solutions for F in terms of variables S0,...,Sn$S_0,...,S_n$ and if the count is < 2^n$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)?

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)?

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)?
Source Link
Grigor Aghanyan
Grigor Aghanyan
  • 83
  • 4

Assignment to make formula unsatisfiable

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)?