How to prove that a constrained version of 3SAT in which no literal can occur more than once, is solvable in polynomial time?
Without loss of generality, we can assume that each variables appears exactly once positively and exactly once negatively (if a variable only appears once set its value to satisfy the clause and remove the clause). We can also assume that a variable does not appear in a clause more than once (if a variable appears both positively and negatively in a clause, then the clause is satisfied and can be removed). These will not alter the satisfiability.

Now use the resolution rule to eliminate the variables one by one (since each variable appears exactly once positively and once negatively this is a deterministic process).  If at any point we obtain the empty clause the set of clauses is unsatisfiable, otherwise it is satisfiable. This is because:


resolution is a complete propositional proof system (i.e. if a clause is logically implied by the set of clauses then it is derivable from the set of clauses using only the resolution rule),
a set of clauses is unsatisfiable iff it logically implies the empty clause.


This algorithm will take polynomial time since each variable is resolved exactly once.  In particular, each application of resolution will reduce the total number of clauses by one, so the number of clauses does not increase.  For example, applying resolution to $(x \lor B) \land (\overline{x} \lor C) \land \dots)$ yields $(B \lor C) \land \dots$, which has one fewer clause than before resolution.  In contrast, if you applied this to a 3SAT formula with no restriction on the number of appearances of each literal, applying resolution could cause the number of clauses to increase exponentially.