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?