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 --&gt; simplifies to A

      A and not B

      A and D 

      B and A

      B and not B --&gt; 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?
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$.