tag:blogger.com,1999:blog-3722233.post3273248546900060061..comments2024-10-03T16:28:40.297-05:00Comments on Computational Complexity: Are there any REAL applications of Graph Isomorphism?Lance Fortnowhttp://www.blogger.com/profile/06752030912874378610noreply@blogger.comBlogger14125tag:blogger.com,1999:blog-3722233.post-64221249828893101312024-02-18T09:15:10.184-06:002024-02-18T09:15:10.184-06:00Update: I found one!
Integer linear solvers use n...Update: I found one!<br /><br />Integer linear solvers use nauty/sassy to handle ILPs with highly symmetric feasible regions, so as to prune the branch-and-bound search tree (eliminating equivalent symmetric subproblems) and speed up the search. See Symmetry Handling in Mixed-Integer Programming by Jim Ostrowski (doi:10.1002/9780470400531.eorms0863) and the topic of "Orbital branching". I confirmed these techniques are applied in the open source solver packages SCIP, CBC/Coin-OR.j2kunhttps://www.blogger.com/profile/08041921049916424212noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-44744093583721496892024-02-17T11:11:53.724-06:002024-02-17T11:11:53.724-06:00I was able to find one software package that menti...I was able to find one software package that mentions the use of GeminiII: https://www.staticfreesoft.com/<br /><br />Looks like it's quite old (last release was maybe in the 2000's?). Meanwhile, I found this on Wikipedia (https://en.wikipedia.org/wiki/Layout_Versus_Schematic):<br /><br />> The need for such programs [comparing circuit layout to schematic] was recognized relatively early in the history of ICs, and programs to perform this comparison were written as early as 1975.[1] These early programs operated mainly on the level of graph isomorphism, checking whether the schematic and layout were indeed identical. With the advent of digital logic, this was too restrictive, since exactly the same function can be implemented in many different (and non-isomorphic) ways. Therefore, LVS has been augmented by formal equivalence checking, which checks whether two circuits perform exactly the same function without demanding isomorphism.<br /><br />This matches my intuition that modern hardware synthesis tools (like, say Yosys or ABC) use SAT solving and formal methods to check for logical equivalence. It's also a sort of "worst case" for an applied math technique when the reason the technique was abandoned is because the technique was not sufficient to solve the underlying problem.j2kunhttps://www.blogger.com/profile/08041921049916424212noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-30794615011649313362024-02-16T19:09:43.101-06:002024-02-16T19:09:43.101-06:00See, e.g.: https://doi.org/10.1109/ICCAD.1988.1225...See, e.g.: https://doi.org/10.1109/ICCAD.1988.122520Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-59554037448267973182024-02-15T20:04:45.201-06:002024-02-15T20:04:45.201-06:00Simply writing code to solve a problem doesnt nece...Simply writing code to solve a problem doesnt necessarily mean it's applied. I would love to hear about the specific places where it's used in formal verification. I was under the impression that was more on the side of SAT solving.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-67607091382336922662024-02-15T19:34:28.855-06:002024-02-15T19:34:28.855-06:00There is practical code for Graph Isomorphism (Nau...There is practical code for Graph Isomorphism (Nauty, see http://users.cecs.anu.edu.au/~bdm/nauty/), which doesn't involve any of the theory of the provably fast algorithms that works very well in practice. Less capable programs were used for years in digital design where edits of circuit layouts would need to be checked quickly to see if no errors were introduced. I know it has been used in formal verification to find automorphisms of logical structures to avoid repeating the same work repeatedly.<br /><br />This practical utility has nothing to do with the recent fast algorithms, which handle "corner" cases that seemed really hard.Paul Beamenoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-76990950568910551652024-02-13T08:05:45.280-06:002024-02-13T08:05:45.280-06:00There is too much misguided emphasis on solving re...There is too much misguided emphasis on solving real-world stuff using exact computation when all we can even ever hope for is a very crude approximation (a fact well known since Newton and Leibniz's days).<br />A two-link simple pendulum is a chaotic system from a physicists perspective but a two-year old with a zillion joints (in an inverted pendulum configuration) can do stairs, ski, skate, bicycle, swim and what not; this person will have occasional trips and falls (the underlying system is no doubt 'chaotic') but will carry on and keep doing all this and so much more till they're 100 years old.space2001https://en.wikipedia.org/wiki/2001:_A_Space_Odysseynoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-41199937915004506912024-02-13T07:49:02.899-06:002024-02-13T07:49:02.899-06:00How does GI play a role in this theorem?How does GI play a role in this theorem?Lance Fortnowhttps://www.blogger.com/profile/06752030912874378610noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-13730406607936914932024-02-12T11:19:13.815-06:002024-02-12T11:19:13.815-06:00Really? 16! ~ 20 trillion. Sounds slow. (My heuris...Really? 16! ~ 20 trillion. Sounds slow. (My heuristic is that usually anything beyond 12! ~ 500 billion is out of scope without a cluster.)Joshua Grochowhttps://home.cs.colorado.edu/~jgrochow/noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-74384701103770800732024-02-12T10:41:25.125-06:002024-02-12T10:41:25.125-06:00There are three reasons why GI is important, two o...There are three reasons why GI is important, two of them have already been mentioned in your post and the comments.<br /><br />1. GI is a universal problem for finite structures in the sense that isomorphism of any finite structure (including groups) can be reduced to GI.<br /><br />2. If GI is not in P, then it resolves the P vs NP question, which could lead to provable one way functions, which are critical for cryptography, which is critical for computer security.<br /><br />If GI is in P, it could show potential vulnerabilities of factoring and other cryptographic functions.<br /><br />3. (If you build it, they will come.) The resolution of GI, which has been open for decades, must need new techniques. These would be directly or indirectly useful for other problems, including cryptography.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-15420234608782420132024-02-12T09:18:45.199-06:002024-02-12T09:18:45.199-06:00(This is Bill) Email me privately to discuss.(This is Bill) Email me privately to discuss.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-88355921056965370012024-02-12T09:14:57.705-06:002024-02-12T09:14:57.705-06:00Hi Bill,
I'm currently in the process of int...Hi Bill, <br /><br />I'm currently in the process of interviewing computational chemists to get to the bottom of this, as one chapter of a book I'm writing (called "Practical Math for Programmers" subtitle: "A Tour of Math in Production Software"). Would you be open to reading that draft and providing feedback?j2kunhttps://www.blogger.com/profile/08041921049916424212noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-44961488082045513522024-02-12T07:26:37.737-06:002024-02-12T07:26:37.737-06:00One moment, LMGTFY :-)
I haven't checked care...One moment, LMGTFY :-)<br /><br />I haven't checked carefully, but the following paper seems to make use of heuristics for graph isomorphism (and contains many images of non-isomorphic graphs along with impressive formulas towards the end):<br />M Borinsky, O Schnetz: Recursive computation of Feynman periods. Journal of High Energy Physics, 2022(8):1-83<br />https://link.springer.com/content/pdf/10.1007/JHEP08(2022)291.pdf<br /><br />To dig up that paper (and many others of similar nature), I used google scholar to find papers that cite Brendan McKays heuristic that implements GI - practical graph isomorphism, II. (IIRC this had been the "latest and greatest" practical implementation some years ago.)Hermann Gruberhttp://www.hermann-gruber.comnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-91977887024093704932024-02-11T22:12:27.835-06:002024-02-11T22:12:27.835-06:00As far as a "practical application", I u...As far as a "practical application", I use graph isomorphism, specifically its implementation in the Python package networkx (https://networkx.org/documentation/stable/reference/algorithms/generated/networkx.algorithms.isomorphism.is_isomorphic.html#networkx.algorithms.isomorphism.is_isomorphic), to code up auto-graded homework assignments for my Theory of Computation course.<br /><br />(Note: networkx does not use Babai's algorithm, it uses something called "vf2"... not sure if that's because Babai's constants are too large to be practical, or if there's some other reason.)<br /><br />For example, I ask the students to do the subset construction to convert an NFA into an equivalent DFA, and I use this package to test, regardless of the names they chose to assign to the DFA states, whether it is isomorphic to the DFA that results from the "official" subset construction algorithm.<br /><br />I'm not sure if grading problems in a course on Theoretical Computer Science, using algorithms developed in Theoretical Computer Science, counts as a practical application of Theoretical Computer Science, but it all feels very practical to me as that autograding code hums away, and the students get their DFAs graded without us having to read over it.<br /><br />Full disclosure: even if Graph Isomorphism required n! time to solve, since we only give the students 4-state NFAs to convert, we could test the resulting 16-state DFAs for isomorphism using the naive brute-force algorithm taking time 16-factorial. But if we did ever decide to be cruel and ask them to convert 20-state NFAs into 20!-state DFAs, we could in principle test those 20!-state DFAs in a reasonable about of time.Dave Dotyhttp://web.cs.ucdavis.edu/~doty/noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-71360471719307439082024-02-11T16:41:14.986-06:002024-02-11T16:41:14.986-06:00"So at one time it was thought that GI would ..."So at one time it was thought that GI would apply to Chemistry. Did it? I suspect some simple algorithms and heuristics did, but (1) chemicals are more complicated than graphs"<br />No problem, the isomorphism of complicated (but finite) structures can be reduced to graph isomorphism. The question you should ask yourself is whether there are real world applications for determining whether two different descriptions of a complicated (but finite) structure actually describe the same structure. I guess the answer is: "yes, but it would be even more practical to get a unique string for each single structure, such that one could hash or do other types of quick database searches". This even more useful operation is called "computing a canonical label". The famous nauty and Traces can do this. In fact, they can do graph canonization (finding a canonical form of a given graph), typically described by a canonical order of the nodes. It is not obvious whether Babai's result transfers to graph canonization, but I have seen remarks that at least it should transfer to "computing a canonical label".Jakitohttps://www.blogger.com/profile/08235089048981338795noreply@blogger.com