great moments in empirical/experimental math/TCS research, breakthrough SAT induction idea

8 Replies

computer-analysis-17512840

update/breaking found 2/19:

hi all, this is a topic Ive been squirreling away links for a very long time, possibly longer than the age of this blog, now about 1½ yr waiting for an opportune moment. such moments can be quite prominent but alas also somewhat rare. am very happy to have recently stumbled on very major one a few days ago that is already getting MSM coverage (did not expect than when 1st writing this entry! wow!) 😀

the blog was started dedicated to TCS and various problems, but also has a very strong empirical flavor based on computational experiments (eg with the collatz conjecture). computer experiments & the interface of math & TCS are an old love of mine that dates to my very earliest uses of the computer & learning its possibilities in teenage years.

joined tcs.se over 2yrs ago and initially was a bit nonplussed by the environment. one of my initial surprises was the lack of interest in computational experiments. the atmosphere/culture is definitely quite specialized at times verging on narrow. the official charter lists TCS as many *broad* topics *in theory* but “in theory, there is no difference between theory and practice, but in practice there is.” for example machine learning is recognized in the charter but gets very little attn on the site (it is the same on cs.se also). theres a new area51 proposal for machine learning, check it out….

however despite some incredible successes such as the 4 color theorem, which to me is unequivocally an advance of empirical/experimental mathematics (more on that later), there is a distinct subculture with a lack of enthusiasm/interest in experimental mathematics and computation in the TCS field. its not exactly an active opposition, but more a disinterest verging on apathy. this can be seen in a few QA on the site. which in research, is basically not much different than a kiss of death.

there are various objections, some real, some imagined/folklore/”urban legend” (or maybe “academic/ivory tower legend”). was able to experience this 1sthand by writing on the subject on tcs.se & getting the immediate skepticism or objections in comments & of course votes which are at times an extraordinarily fine-tuned measure of collective interest/attention of the “group mind”.

the zeitgeist tipping point for me to write up a few of these thoughts was Gowers announcement of the recent breakthrough computational SAT results on the Erdos Discrepancy Problem by Konev & Lisitsa. 😯

this is a very old/deep problem in mathematics that relates to trends in infinite random sequences and in some ways reminds me of the Collatz conjecture (and also the Riemann hypothesis). showing the deep links between all of these 3 problems would be a fun exercise, but not for today (and Im nearly totally unqualified for it anyway!). even better a lot of the worlds best math/TCS bloggers are fascinated with the erdos discrepancy problem eg RJL, Kalai, Windows on Theory, Tao, etc. and it was a polymath problem not long ago! 😎

Bailey & Borwein are some excellent writers on the subject of experimental mathematics. they do not address the TCS angle too much. it would be very beautiful if a companion type ref existed from a TCS angle of using SAT to attack theoretical problems using empirical approaches, but alas none such ref seems to exist today.

the recent Simons article profile on Zeilberger by Wolchover captures some of the significance of the field. Zeilberger has been cranking away almost singlehandedly for many years. it would be really great if there was a survey of his results. havent seen one.

in oct 2013 the Bundala/Zavodny paper finding optimal sorting networks via SAT appeared. have seen zilch reaction so far to this paper. anyone else? this to me is a breakthrough result that definitely presages the Konev/Lisitsa results but nobody seems to have noticed so far. this resolves a 4 decades old conjecture by Knuth. hey isnt this nearly award winning stuff? ❗ isnt anyone paying attn? dont know! talked about it in tcs.se chat but there was only dead silence. [not that there was anything different about that response, 😛 ]

another nice paper in this line of results using SAT solvers that popped out at me is the Cook/Etesami/Miller/Trevisan paper on analyzing hardness of one-way functions. this has some very tricky analysis that frankly, to me doesnt look like that far from a P≠NP proof. (drunk & myopic algorithms? huh? sounds like tcs.se to me!) at the end, almost as a semi embarrassed afterthought they mention that they did SAT experiments to back up their theoretical results.

recently on tcs.se the use of Answer Set Programming to attack a very difficult conjecture was applied. this looks like a very sophisticated new use of SAT type solvers applied to more higher level proof problems such as involving math objects like graphs & graph properties etcetera. predict a very big future for this type of research in resolving some real difficult mathematical problems but right now it all seems to largely be flying “below the radar” of more mainstream research.

including a link by Sedgewick on “empirical analysis of algorithms” in Java, which amazes me how rarely this exercise is employed by CS students. just graphing execution time of a program seems not to be regarded as a highly worthwhile exercise. huh! what do I know about education anyway!

RJL recently had a blog on “black vs white boxes” about the difference between “how” questions and “why” answers and how this applies to mathematics. to me SAT and NP complete problems are at the heart of this ancient concept.

could write much more in detail & commentary on all this but this is a blog so will have to leave some to the imagination, and my odds are that nobody will reply to this in comments anyway! 😥

💡 💡 💡

LittleComputerone last thought. a very extraordinary idea occurred to me years ago, and am starting to get a better picture/handle on it. imagine that you have some question/property that relates to an infinite number of mathematical objects, each of finite size. typically you might want to verify this property holds for finite size objects of increasing size and then somehow attempt to “manufacture” or “create” a proof out of the analysis results on each of these separate objects.

so more formally, imagine a set of SAT formulas f_1, f_2, ..., f_n that verify your property. each f_n is finite size, but n approaches infinity. now you want to run experiments and verify your property. you run your SAT solver and it proves that there is no solution, or a solution, to f_1, f_2, f_3, ... for some finite cases. but you want to find a pattern between these solutions, and then find an inductive proof that captures this pattern, and then shows how to reapply the SAT solver to each f_n to get a solution or prove a nonsolution.

that to me is a very deep idea, one at the heart of computational induction, and hinted in these papers looking at SAT instances. came up with some of these concepts over a decade ago but havent had the time to pursue them myself. it appears still nobody has been researching this particular use of SAT solvers so far.

need a nice shorthand term for this. how about “SAT induction”? suspect even very difficult problems could be attacked this way. in fact just after reading about Bundala/Zavodnys results, remembered this idea and then came up with an entire mental picture of how to try it out on the collatz conjecture. (years ago had ideas of applying it to the P=?NP question).

this is a research program in the sense referred to by RJL in his great blog on the subject.

hey seriously this stuff is revolutionary, @#%& dont you see it? did you miss it? just there described er *sketched out* the future of 21st century mathematics/TCS breakthrus ❗

anyone following that? anyone with me on this? its *brilliant* right?!? someone could take over the world with an idea like that, eh? its a *proof-inator!* 😈 have been looking for collaborators… only a few decades! 😥

have an intention to eventually try out these ideas someday but it will take a few weeks of work at least to make a serious dent in this line of attack. however, have long thought there could be a real breakthrough payoff lurking in this direction. juicy & ripe for the plucking…? a great polymath prj if you ask me 😀 but as an illustrious cs.se mod R. recently pointed out/reminded in chat, nobody *did* ask me, & anyway dont have a shiny fields medal to overwhelmingly persuade ppl to follow it… 🙄

ps will work for feedback! the above text was banged out quickly & needs to be ref’d more meticulously with the links below, but hey real science like that is timeconsuming! whoever writes an intelligent comment & requests citing, will respond by adj’ing this article with cite numbering & fleshing out ideas a bit more.

a. experimental/empirical math/TCS

b. books

c. (t)cs.se/MO q/a empirical/experimental math/TCS

8 thoughts on “great moments in empirical/experimental math/TCS research, breakthrough SAT induction idea”

  1. marziodebiasi

    I saw the link on cstheory and I read your post (funny the colloquial style 🙂 ), but didn’t grasp exactly the core of your idea. I think you should explain with much more details (and formal notation) what do you exactly mean with “SAT induction”; and (if the case) how you face the boolen equivalence and boolean isomorphism problems that are themselves “hard” problems (the first NPC the second coNP-hard).

    Reply ↓
    1. vznvzn Post author

      hi MdB thx much for cogent response. yes even though its clear in my head alas it is maybe a tricky idea that is difficult to communicate so far & it doesnt look like (at least from comments) anyone quite understands it yet. need to work up a more illustrative example. did you see my comment re OR of functions? did you upvote the question? note that generalized induction is basically undecidable, so “reducing” it in some way to machine learning plus maybe computationally intractable (but not undecidable) problems is potentially a breakthrough. can expound more at length in tcs.se chatroom if you have some spare moments over time.

      Reply ↓

  2. Pingback: the joy of (cyber) mathematics | Turing Machine

  3. Pingback: collatz “pseudo induction” contd, trials & tribulations of wordpress hacking/ blog code inclusion | Turing Machine

  4. Pingback: Terence Tao magic breakthrough again with EDP, Erdos Discrepancy Problem | Turing Machine

  5. Pingback: select refs and big tribute to empirical CS/ math | Turing Machine

  7. Pingback: collatz finetuning | Turing Machine

Leave a comment