Oracle that can only definitively say if an instance is unsatisfiable

Question

Assuming I have an Oracle that takes as input a strictly 3SAT Boolean instance and states whether the instance is satisfiable or not. If it says instance is unsatisfiable then the instance is unsatisfiable. If it says instance is satisfiable there is a 57% chance the instance is satisfiable and a 43% chance that is unsatisfiable. The percentages are just an example, essentially oracle is reliable only one way.

Can I use such an Oracle to solve 3SAT instances? If so, how?

Answer 1

You can use your oracle to construct a process that is guaranteed to be correct, and will most likely be fast.

The basic idea is that a proof that a formula is unsatisfiable might be huge - but if that's the answer we get, we can trust it. On the other hand, we can easily convince ourselves that the formula is satisfiable by inspecting a satisfying assignment.

As pointed out by Nathaniel, we can get our correctness chances arbitrarily close to 1 by just making a constant number of oracle calls, and answering "satisfiable" only iff all of them say so.

Now the procedure is as follows:

1. Ask the oracle if the formula is satisfiable. If "no", we are done.
2. Substitute $x_0 = \top$ and $x_0 = \bot$, and ask for both resulting formulae whether they are satisfiable. If both answers are "no", the originl formula is not satisfiable. If exactly one says "yes", proceed with that formula. If both say "yes", proceed with $x_0 = \bot$ and keep $x_0 = \top$ for backtracking.
3. Once values for $x_i$ for $i < j$ have been chosen, try $x_k = \bot$ and $x_j = \top$. If both substitutions yield "no", go back to back to the last backtracking point. If one says "yes", proceed with that one. If both say "yes", create a backtracking point.
4. Once all variables are instantiated, check whether you have a satisfying assignment. If so, the original formula is satisfiable. If not, backtrack.
5. If you are supposed to backtrack, but there is no backtracking point, the original formula is not satisfiable.

The procedure will never give us a wrong answer. Its worst-case runtime is exponential, but every time we backtrack this is due to our oracle incorrectly answering "satisfiable", which is very unlikely. Using Wolfram Alpha for the calculation, I get that the expected number of backtracks is below 1.4 for a oracle correctness probability of 0.9. It follows that the expected runtime of the procedure is linear.

Answer 2

Edit: I wrongly read the question, therefore the following answer is incorrect. It would be correct if the oracle worked as followed: "if the instance is unsatisfiable, then the oracle always says it is unsatisfiable otherwise, there is a 57% chance the answer is that the instance is satisfiable, and a 43% chance that it is not".

The key here is to repeat the process of asking your oracle to improve the probability of getting the right answer. You know that the way it is constructed, if the oracle states that a formula is satisfiable, then IT IS satisfiable (since it never makes mistakes on non-satisfiable formulas).

For example, with your percentages, if you ask 6 times your oracle if a formula $\varphi$ is satisfiable, it will always give the right answer if $\varphi$ is not satisfiable, and there will be over 99% chance to say that $\varphi$ is satisfiable if $\varphi$ is satisfiable, because it has $0.43^6 < 1\%$ chances to say that $\varphi$ is not satisfiable even if it is.

You will never be able to guarantee 100% in both cases, but you can be as close as you want by repeating the question to the oracle.