tag:blogger.com,1999:blog-6555947.post1187765454327736034..comments2024-03-14T01:32:43.610-06:00Comments on The Geomblog: NSF EDA Workshop: Wrap upSuresh Venkatasubramanianhttp://www.blogger.com/profile/15898357513326041822noreply@blogger.comBlogger10125tag:blogger.com,1999:blog-6555947.post-54457010827315339562009-07-09T19:40:06.967-06:002009-07-09T19:40:06.967-06:00Also, I am not sure what you would do if I gave yo...<i><br />Also, I am not sure what you would do if I gave you an oracle that could solve all 1000 variable SAT instances. :)<br /></i><br /><br />Oh, I'd probably have more fun with a 1000-variable SAT solver than I would writing an NSF grant proposal with a working title of "Why people who solve formal verification problems are less miserable than theoretical computer scientists think they should be." (Of course, that title would have to change in the final draft.) But to each his own.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-6555947.post-52859540516587878712009-07-09T19:00:45.866-06:002009-07-09T19:00:45.866-06:00I'd rather have a SAT solver that solves all i...<i> I'd rather have a SAT solver that solves all instances up to 1000 variables than one that does special cases of 10000-variables instances.</i><br /><br />I don't think we should discount these solvers. Yes they may not solve your R(k,k) problem, or your factoring problem, but they are actually great at solving a large number of real problems. I think formal verification is one great example: they can often phrase the problem of checking correctness of a program as a SAT instance and these SAT solvers work great and are used in practice.<br /><br />Also, I am not sure what you would do if I gave you an oracle that could solve all 1000 variable SAT instances. :)Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-6555947.post-25297173010078503132009-07-09T18:26:06.405-06:002009-07-09T18:26:06.405-06:00Indeed. and see Michael Mitzenmacher's comment...Indeed. and see Michael Mitzenmacher's comment at Dick Lipton's blog:<br /><br />http://rjlipton.wordpress.com/2009/07/09/nsf-workshop-summary/#comment-912Suresh Venkatasubramanianhttps://www.blogger.com/profile/15898357513326041822noreply@blogger.comtag:blogger.com,1999:blog-6555947.post-68621817507877877382009-07-09T18:24:22.560-06:002009-07-09T18:24:22.560-06:00Fair enough. I'd rather have a SAT solver tha...Fair enough. I'd rather have a SAT solver that solves all instances up to 1000 variables than one that does special cases of 10000-variables instances.<br /><br />I guess the theory question would be: can the instances of SAT that they're interested in be "reduced" to problems known to be in P? My guess is yes but it's easier for them to write them as SAT problems.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-6555947.post-15144968026674656412009-07-09T18:01:17.256-06:002009-07-09T18:01:17.256-06:00ok. so that's what I thought you meant. Rememb...ok. so that's what I thought you meant. Remember that I didn't say that they could solve ALL 10,000 variable instances (as an aside, I actually forget the upper limit of what they can solve). They have solvers that can solve a number of large instances that arise in practice, and one question that they'd like to understand is why some instances are solvable and some aren't.Suresh Venkatasubramanianhttps://www.blogger.com/profile/15898357513326041822noreply@blogger.comtag:blogger.com,1999:blog-6555947.post-54864118424132087552009-07-09T17:57:20.005-06:002009-07-09T17:57:20.005-06:00Sure. The question "does R(k,k) = n?" c...Sure. The question "does R(k,k) = n?" can be phrased as a SAT problem with n choose 2 variables and 2(n choose k) clauses. Assign each edge in K_n a variable so that false is red and true is blue. For each k-clique in K_n, create two clauses to constrain the variables so that not all the variables can be equal. If you can satisfy the formula, then you have a two-coloring where there is no monochromatic k-clique and thus know that R(k,k) > n. If it is unsatisfiable, then you know R(k,k) <=n. <br /><br /><br />Now, R(5,5) is unknown. But we do know that 42 < R(5,5) < 49. Thus can see that the SAT formula involved in pinning the number down have much less than 10,000 variables. I don't think any SAT solver can answer that at the moment. <br /><br /><br />Wow...moderating comments at 37,000 feet is cool! You might be the first blogger in history to do this!Unknownhttps://www.blogger.com/profile/10522742342177873731noreply@blogger.comtag:blogger.com,1999:blog-6555947.post-46548664699623410602009-07-09T17:35:10.276-06:002009-07-09T17:35:10.276-06:00anon: I'm a little confused about your comment...anon: I'm a little confused about your comment. could you clarify ?Suresh Venkatasubramanianhttps://www.blogger.com/profile/15898357513326041822noreply@blogger.comtag:blogger.com,1999:blog-6555947.post-58365335865121473392009-07-09T17:32:55.170-06:002009-07-09T17:32:55.170-06:00"They also talked about providing benchmarks:..."They also talked about providing benchmarks: for example, a 10,000 variable SAT instance and code that solves it."<br /><br />Right.... Then as a theorist you can show how if they had that, they could answer unsolved problems in Ramsey theory very quickly and be heroes of the discrete math community. R(5,5) and R(6,6) would be resolved immediately. <br /><br />Let me know who's up to the challenge. I'll give them the SAT instances (if you haven't figured them out already.)Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-6555947.post-89649315850356893822009-07-09T17:21:13.631-06:002009-07-09T17:21:13.631-06:00We need a way to link comments across blogs !
To...We need a way to link comments across blogs ! <br /><br />To answer your question, Michael, my understanding is this is part user driven and part problem driven.<br /><br />From the system perspective, there's an entire pipeline of components that go into making a design, and they like to fiddle with these pieces repeatedly (the incremental part). Having a randomized element that could change its answer the next time the whole pipeline is compiled is a problem.<br /><br />Now this can be changed with a litte tweaking: as you mention, as long as the seed can be preserved, an algorithm can be run in "randomized" or "deterministic mode": in the latter form, it merely uses the cached seed. <br /><br />But here's the user side of the story. They want these designs to be portable across different machines/systems, so that different users, running with the same "knobs", get similar answers.<br /><br />This is because the user of such a tool is faced with a bewilidering array of knobs, and over time has become accustomed to setting certain knobs a certain way. Changing things around makes them unhappy. <br /><br />Now this latter problem is sociological, and is difficult to deal with for us. But I suspect the best approach is to ignore it for now. It's really the companies that are concerned with satisfying their user base, and it's not clear to me why research-level tools need to live under the same constraints. My personal view is that the underlying facilitating technologies for EDA research appear to be very tied to corporate products, and this is somewhat of a problem. To me it's as if all database researchers had to use Oracle, and couldn't really complain about it if it wasn't very useful. <br /><br />I will also Cc this over at @rjlipton.Suresh Venkatasubramanianhttps://www.blogger.com/profile/15898357513326041822noreply@blogger.comtag:blogger.com,1999:blog-6555947.post-80536406945775248872009-07-09T15:11:52.490-06:002009-07-09T15:11:52.490-06:00I admit some confusion as to why "randomness&...I admit some confusion as to why "randomness" is considered such a problem? In the real world, usually randomness is pseudo-randomness (often something simple, perhaps lacking in provable properties but functional nonetheless), and you can essentially make your "randomized algorithm" deterministic by remembering the small seed. So why is randomness going to be a problem?<br /><br />(I'm not being flip -- I'm really interested! If they view it as a problem, there's probably some research to be done to make it not a problem in this context.)<br /><br />I'm cc'ing the comment at Lipton's blog...Michael Mitzenmacherhttps://www.blogger.com/profile/02161161032642563814noreply@blogger.com