It is known that random k-SAT instances with at least $cn$ clauses, where $c =\nobreak c_k$ is a suitable constant, are unsatisfiable (with high probability). We consider the problem to certify efficiently the unsatisfiability of such formulas. A backtracking-based algorithm of Beame et al. [SIAM J. Comput.,} 31 (2002), pp. 1048--1075] shows that k-SAT instances with at least $n^{k-1}/(\log n)^{k-2}$ clauses can be certified unsatisfiable in polynomial time. We employ spectral methods to improve on this bound. For even $k\ge 4$ we present a polynomial time algorithm which certifies random k-SAT instances with at least $n^{(k/2)+o(1)}$ clauses as unsatisfiable (with high probability). For odd k we focus on 3-SAT instances and obtain an efficient algorithm for formulas with at least $n^{3/2+\varepsilon}$ clauses, where $\varepsilon >0$ is an arbitrary constant.

A resolution proof of an unsatisfiable propositional formula is called regular if and only if no variable is eliminated (with the resolution rule) twice on any branch of the proof tree representing the resolution proof. An infinite family of unsatisfiable propositional formulas is constructed and the following shown: These formulas have polynomial size unrestricted resolution proofs, whereas all regular resolution proofs of these formulas are of superpolynomial length.

Higher type primitive recursive definitions (also known as Godel's system T) defining first-order functions can be classified into an infinite syntactic hierarchy. A definition is in the nth level of this hierarchy, a so-called rank-n definition, if and only if n is an upper bound on the levels of the types occurring in it. The author interprets these definitions over finite structures and shows that rank-2 definitions characterize PTIME, rank-3 definitions characterize PSPACE, and rank-4 definitions EXPTIME.>