Automated theorem proving with SAT
If you believe that a proof or disproof has reasonable length, you could come up with one SAT instance which states $x_1,\ldots,x_n$ encodes a proof of the Riemann Hypothesis, and another one stating $x_1,\ldots,x_n$ encodes a refutation of the Riemann hypothesis. The formula will have size polynomial in $n$, though probably not linear; if you're careful, maybe quasilinear ($n\log^{O(1)}n$). You can then apply your magic SAT solver to find out which, if any, of these options is correct. Don't hold your breath, though – as mentioned in the comments, it is hard to imagine an algorithm which would be efficient enough to handle the required value of $n$ in a realistic amount of time.