Consider the following special case of SAT, which we will call koccurrence-SAT for a fixed parameter k N. The input consists of a SAT formula f(x1,...,xn) in CNF such that every variable xi appears (as is, or negated) in at most k clauses. The problem is to decide whether there is a satisfying assignment. For k = 3, either (a) design and analyze a polynomial time algorithm, or (b) show that a polynomial time algorithm for k-occurrence-SAT implies a polynomial time algorithm for (CNF-)SAT.