# 3SAT with an oracle for expanding the clauses

Let's consider 3SAT, so we have clauses like:

(A or B or C) and (A or not B or D) and ...

If we distribute the "and" over the first two clauses, we get the disjunction of:

      A and A --> simplifies to A

A and not B

A and D

B and A

B and not B --> simplifies to false

B and D

C and A

C and not B

C and D


I presume the brute force strategy of expanding all the clauses and simplifying when possible would take exponential time. My question: what if an oracle gives you a certificate telling you which clauses to expand? Is it known whether this could get you down to polynomial time?

Let's call this language 3SAT^A, so it's something like: 3SAT^A = {(x, A(x)) : x is a 3SAT formula}, where A(x) tells you how to expand the clauses in x.

Is it known whether there is an A such that 3SAT^A is in P? If so, could one hope to show P != NP by showing that no such A is computable in polynomial time?

• Please give an example of "a certificate telling you which clauses to expand" ? – Kyle Jones Dec 22 '15 at 23:36
• So, for example, if n is the number of clauses, then a certificate would be a list of pairs (i, j) with the first (i, j) such that i, j <= n, the second (i,j) such that i, j <= n - 1, and so on. First expand clauses 17 and 23, then renumber the clauses (since there are now n-1 instead of n), expand clauses 5 and 32, etc. – Brian Dec 23 '15 at 12:27
• This could have exponential blow up on the yes-side, since a disjunctive normal form formula could be exponential. However, it's not clear what happens on the negative side, since eventually a formula with no satisfying assignments will reduce to false. – Brian Dec 23 '15 at 12:29

Your question seems closely related to the question of whether $NP=coNP$. It seems that the existence of such an oracle would imply $NP=coNP$ since the oracle would give you a polynomial certificate for "no"-instances of $SAT$.
I don't think this would be a viable way to show $P\not = NP$ since all you'd be showing is that there's no way to expand clauses in polynomial time, but that does not rule out other approaches for solving $SAT$.