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?
$\begingroup$
$\endgroup$
3
-
1$\begingroup$ You couldn't. Those require something stronger than SAT (first-order logic, etc.). $\endgroup$– D.W. ♦Commented Jul 13, 2014 at 2:53
-
$\begingroup$ 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. $\endgroup$– vznCommented Jul 13, 2014 at 5:41
-
$\begingroup$ And even if you could (but see the comment by @D.W.), a "polynomial time algorithm" is not necessarily a practical one at all. $\endgroup$– JuhoCommented Jul 13, 2014 at 14:55
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
1
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.
answered Jul 15, 2014 at 3:08
-
$\begingroup$ There is only one Riemann Hypothesis, so its proof is of constant length, so it can be verified in constant time, regardless of the complexity of SAT. And how do I come up with that proof, anyway? $\endgroup$ Commented Jul 15, 2014 at 8:34