NSF Workshop Summary
The second day of the NSF workshop on role of theory in design automation
Lynn Conway, with Carver Mead, also played a major role in the VLSI revolution. She is the other half of the creators of the Mead-Conway revolution. This workshop would not be happening if it were not for her wonderful work.
Today I want to summarize the last half day of the NSF workshop. We had multiple breakout groups to discuss what should NSF do in this area.
I once stayed at the Hilton next to NSF for another panel. As many hotels like to do, this Hilton had a computer monitor with the events of the day displayed. I looked up and saw the following on the monitor:
Bureau of Prisons: Breakout Sessions 10am-11am.
I cracked up and pointed this out to my colleagues. I think they smiled, but did not find it as funny as I did. Oh well.
Our Group Discussions
There was a discussion on one of the big puzzles in theory : Why do SAT solvers of various kinds work so well in practice? It was pointed out that real-world problems seem to be easy to solve with various SAT solvers. So what does this mean for P=NP?
There was a long discussion on stochastic systems. Perhaps this can be linked with the theorists who work on Rapidly Mixing Markov Processes. Many of the future design problems are stochastic for a variety of reasons. How do we check the properties of such systems? Applications include reasoning about power consumption of chips or biological systems, since such systems are not deterministic.
Theory Report
Vijaya Ramachandran and Suresh Venkatasubramanian and I were charged with putting together a half hour report on what role theory can play in design automation. We divided the report like a bad version of Charles Dickens’ Christmas Carol: I did the past, Suresh the present, and Vijaya the future.
All Hands Discussions
Here are the reports from the four group leaders of the breakout groups. Well not their reports, but some high level view of what they had to say.
A very hot topic, this is a bad pun, is that there are power viruses that use power to destroy a chip. The idea is suppose there is a strange program that if executed will cause way beyond the planned power consumption. If this can happen, then a virus can destroy your chip. Quite an interesting security question. Can you say cyber-warfare?
Open Problems
One of the recurrent themes of the discussion is: we have SAT solvers that seem to work on all examples we try them on. How does this fit with the conventional wisdom that P
Last post on NSF. Back to usual for next post.
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?
(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.)
Comment cc’ed at Suresh’s blog.
We need a way to link comments across blogs !
To answer your question, Michael, my understanding is this is part user driven and part problem driven.
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.
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.
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.
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.
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.
Cc’d over at my place.
Richard — your open question regarding the solvability of SAT reminded me of my paper with Salil Vadhan on “Why Simple Hash Functions Work”, where we were tackling a similar question in that there seemed to be a gap between practice and what the theory seemed to be telling us. There the “answer” seemed to be that if we assume the sequence of items being hashed has “enough entropy” for some notion of enough (and some notion of entropy), then even very simple hash functions suffice to get near-uniform performance.
I wonder if something similar could work here? We do have provable performance guarantees for sparse random k-sat formulae, for instance. Perhaps real-world instances have enough entropy that they look enough like random formulae to suffice for these algorithms?
This is why I was intrigued by the offer to provide “real-world” instances of SAT that are “easy to solve” by a solver. Having a db of such instances might make such investigations feasible.
I really like the idea of trying to prove if as you say there is enough entropy then SAT solver will work.
We should talk about this, would be a cool result.
E-mail me and let’s get started! 🙂
I think to start I’d have to review why the “standard SAT algorithms” happen to work. Way back when I worked on the “simplest” algorithm — the pure literal rule — but I’m not that up on my backtracking algorithms.
I wonder if the threshold has anything to do with this: i.e being dense versus being close to the 4.2 ratio for clauses/variables.
I thought it was well known that SAT solvers fail miserably on precisely the problems where you really wish they would work well (e.g. integer factoring, cryptanalysis, etc). Is that not the situation?
The answer is probably yes. But have people tried it? Note it also might be important exactly how the problem is encoded into SAT.
Ilya Mironov at Microsoft Research Silicon Valley had a neat paper with his colleagues on finding hash collisions using SAT solvers.
http://research.microsoft.com/en-us/people/mironov/sat-hash.pdf
Despite encouraging results on MD4 and MD5, the technique has not so far progressed to finding collisions in SHA-1. It’s also worth noting that the solver in this work is used in a specific way that depends on a human first discovering a “differential path” for a particular hash function that is likely to lead to easy collisions. There is some work prior to Mironov’s that tries to brute force the collision search problem by directly encoding into SAT, but if I remember correctly such attempts failed even on MD4.
On the other hand, 90+% of all the instances I see in my “whitebox fuzz testing” work turn out to be solvable within seconds. So there is certainly an issue of hidden structure here.
http://www.cs.berkeley.edu/~dmolnar/metafuzz-tr-draft.pdf
ftp://ftp.research.microsoft.com/pub/tr/TR-2007-58.pdf
Moreover, I don’t think the EDA folks particularly care about those examples.
I agree with Suresh. Their SAT instances are probably the SAT-encoded version of “given an array, is it sorted?” If it’s sorted, then it’s satisfiable, otherwise it is unsatisfiable.
It appears that the SAT instances from EDA applications are quite structured
and far from “random” because they come from circuits typically designed in a hierarchical fashion by either people or automated design tools. I wonder if looking towards entropy/random SAT analysis is the right thing to do. Just a thought, I am not familiar with the domain but I had a conversation with Igor Markov at some point along these lines.
Yes, I believe cryptographers have tried SAT solvers on ciphers and hash functions, and gotten nowhere. It sounds to me like EDA (circuit routing) simply gives rise to easy problem instances. After all, you get the sorts of component layouts that humans can usually figure out with enough effort. Maybe it can also be compared with protein folding, which is NP-hard but which is “solved” by nature in cell reproduction all the time–as Scott Aaronson points out, again because the instances that arise in natural biology are easy. Heck, maybe even mathematics is like that. Serious mathematicians like Hilbert believe until the 1930’s (Gödel’s theorem) that all math problems were not only solvable, but were solvable by humans.
Here’s an article about trying Minisat on AES:
http://cs.swan.ac.uk/~csmg/2009_BCTCSWarwick_MG.pdf
Actually, this one might interest you more. It’s about random formulas:
http://www.cs.swan.ac.uk/~csoliver/Artikel/OKsolverAnalyse.html
I found both (and others) through: http://www.google.com/search?q=“sat+solver”+aes
I thought the standard explanation for why SAT solvers work well “in practice” is that they are applied to instances that come from “modular” designs (for example in the case of VLSI or software verification), this modularity translates into instances of low treewidth, and SAT is provably easy on low-treewidth (and related non-expansion measures) instances.
I think that this amy be part of the answer, but cannot be hold story. Crypto boxes, like AES, are very well structured and made out of modules. So why is it so hard to break them with SAT solvers?
I think this is a really interesting challenge. I like Mike (Mitzenmacher) ideas about entropy a lot. Still a mystery to me.
I am curious. Is there any known SAT solver that when given a SAT instance with bounded treewidth terminates in polynomial time (it could take n^{f(k)} time where k is the treewidth)? Basically it should work without having a tree decomposition.
Interesting question. I assume that you mean something like: take a “standard” SAT solver. Can we prove that for treewidth k, the algorithm runs in time exponentially only in k?
This is actually known. Specifically, construct a graph for a SAT instance where variables are nodes and two variables are connected if they occur in the same clause. Then if this graph has treewidth k, then there exists an algorithm for solving SAT that runs in time nk2^k.
In other words, SAT parametrized by treewidth is in FPT.
Ref: http://courses.csail.mit.edu/6.854/06/scribe/s22-online.pdf
So I misunderstood slightly. The algorithm I mentioned above requires the tree decomposition, so it won’t work “obliviously”.
About AES, I think that because of the “diffusion” steps, if you reduce the task of breaking AES to a SAT formula you would get a formula in which the clause-variable graph has noticeable expansion and, definitely, high treewidth. (So “modularity” is not sufficient for the formula to be easy, it should also be true that the modules have “small interface” and that the modules themselves recursively have a modular structure.) I don’t know, unfortunately, of any experimental study of the treewidth (or related parameters) of large SAT formulas that are solved efficiently in practice.
I have heard (but I don’t know of references) that SAT solvers that are good in practice do not do well on random instances of density slightly below the threshold. (Very sparse random instances are easy to satisfy by fairly trivial heuristics, but the satisfiable regime close to the threshold is tricky.) It is conjectured that the survey propagation algorithms solve random instances of any density below the threshold, but Dimitris Achiloptas discussed some evidence against the conjecture at the Princeton Cryptography/Complexity workshop in June. In any case the “practical” SAT solvers don’t do well on random instances.
Please see the paper
http://www.lsi.upc.es/~atserias/papers/clauselearning/aft_sat_paper_llncs.pdf
for results on SAT solvers and bounded treewidth.
Thanks. The paper is quite relevant to the discussion.
There is a website SAT Live! that has links to a wide variety of benchmark SAT problems, many of which were contributed as part of annual SAT-solver competitions. It is a little misleading to discuss items like numbers of variables for the formulas since many are derived by standard translations that generate many variables that don’t show up outside of 2-clauses. It is true that problems involving tens of thousands of variables are solved routinely by forms of backtracking search. On the other hand such methods fail on satisfiable random 3-CNF formulas with only 500 variables and 2050 clauses (whereas a metropolis-style local search will handle 100,000-variable formulas at the same clause-variable ratios and survey propagation will handle 1,000,000-variable formulas at the same ratios). Unfortunately, survey propagation seems useless on practical problems (it cannot handle large arity constraints well) and local search does not compete well with backtracking search for most such problems.
A major win in moving to SAT solvers for tasks such as analyzing AES is that the solution methods are so simple and flexible that they do not get so bogged down in the structural details. On the other hand, most of the effective backtracking routines are, at heart, only efficient engines for resolution inference and as such have the inherent limitations of resolution inference.
LCD monitors are the de factor standard these days because they do not consume too much electricity`;~