Let we have a 3CNF under following restriction: each variable occurs 3 times.
Then I apply generalized resolution (GR) (I don't know which name would fit more) technique (number of clauses can be arbitrary large, just an example):
$(x\lor A)\land(x\lor B)\land(\overline x\lor C)=(A\lor C)\land(B\lor C)$. Here $A,B,C$ are some clauses. Neither $A$ and $C$ nor $B$ and $C$ have opposing literals (like in original resolution, the reason is not to exponentially increase length of formula).
Is it an open problem if there is such a sequence of choices (which variable to choose for GR) that will return 'NO' if formula is unsatisfiable? Or there is a proof that some unsatisfiable formulas (with given restrictions) have no such sequences? Meaning that for every pair of literals $x,y$ on some step it will be possible to find a clause $(A\lor x\lor y)\land(B\lor\overline x\lor\overline y)$.
We assume that we can use any known polynomial technique such as unit propagation, absorption rules $(x\lor A)\land(\overline x\lor A)=A; A\land(x\lor A)=A$, pure literal rule (if variable always occur as positive or negative, remove all clauses where it is contained), changing equal literals, finding strongly connected components in a graph for 2-clauses, etc.