A simple first moment argument shows that in a randomly chosen k-SAT formula with m clauses over n boolean variables, the fraction of satisfiable clauses is 1−2−k +o(1) as m/n → ∞ almost surely. In this paper, we deal with the corresponding algorithmic strong refutation problem: given a random k-SAT formula, can we find a certificate that the fraction of satisfiable clauses is 1 − 2−k + o(1) in polynomial time? We present heuristics based on spectral techniques that in the case k = 3 and m ≥ ln(n)6 n3/2 , and in the case k = 4 and m ≥ Cn2 , find such certificates almost surely. In addition, we present heuristics for bounding the independence number (resp. the chromatic number) of random k-uniform hypergraphs from above (resp. from below) for k = 3, 4.