# Automated theorem proving with SAT

If you had a polynomial time algorithm for determining boolean satisfiability how would you prove/disprove a conjecture like the Reimann-Zeta hypothesis (or the Pythagorean theorem for that matter) from axioms?

• You couldn't. Those require something stronger than SAT (first-order logic, etc.). – D.W. Jul 13 '14 at 2:53
• SAT was recently used on the Erdos Discrepancy Problem with some success and its also being used to construct small optimal sorting networks, solving long open problems of Knuth. do think/conjecture that this will expand & there will be more powerful uses of SAT in the future incl induction over infinite values, but so far its barely even a twinkle in anyones eye. – vzn Jul 13 '14 at 5:41
• And even if you could (but see the comment by @D.W.), a "polynomial time algorithm" is not necessarily a practical one at all. – Juho Jul 13 '14 at 14:55

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.