Summary: In this paper, we prove a lemma that shows how to encode satisfying solutions of a $k$-CNF (boolean formulae in conjunctive normal form with at most $k$ literals per clause) succinctly. Using this lemma, which we call the satisfiability coding lemma, we prove tight lower bounds on depth-3 circuits and improved upper bounds for the $k$-SAT problem. We show an $Ω(n^{1/4}2^{\sqrt{n}})$ lower bound on the size of depth-3 circuits of AND, OR, NOT gates computing the parity function. This bound is tight up to a constant factor. We also present and analyze two simple algorithms for finding satisfying assignments of $k$-CNFs. The first is a randomized algorithm which, with probability approaching 1, finds a satisfying assignment of a satisfiable $k$-CNF formula $F$ in time $O(n^2 |F|2^{n-n/k})$. The second algorithm is deterministic, and its running time approaches $2^{n-n/2k}$ for large $n$ and $k$. The randomized algorithm improves on previous algorithms for $k>3$, though subsequent algorithms improve on it; the deterministic algorithm is the best known deterministic algorithm for $k>4$.