Dynex SAT solver moving goal posts
Recently there has been some discussion on SAT solvers around the Dynex cryptocurrency project. The Dynex project claims to have invented a new computing paradigm with powerful buzzwords like neuromorphic computing and simulated digital memristors being thrown around in their marketing like there is no tomorrow. It sounds very fascinating. Really.
One of the flagship claims of the Dynex project is their Dynex Neuromorphic Chip SAT solver. It was claimed to be revolutionary, showing results from another world. That was, until somebody tried a real existing solvers (YalSAT and PalSAT) on those problems. The results were reported to the Dynex project and that ended up in a game of whack-a-mole:
Mole 1: YalSAT beats the infinitely superior Dynex SAT Neuromorphic solver
Whack 1: Add more benchmark input that work better with Dynex SAT and “prove” it is superior.
Mole 2: Parallel solver PalSAT beats Dynex SAT in their new benchmark suite
Whack 2: Delete the issue and add own optimised three thread results. Victory!
Mole 3: Question why choose 3 threads to make Dynex look good and not 8 threads?
Whack 3: Modify the ticket out of context and not comment anything.
Mole 4: Why delete ticket? Why not explain reasoning for choosing 3 threads for PalSAT vs. Dynex SAT?
Whack 4: Do nothing, ignore.
That game ended there as you can’t play ball without an opponent.
Moving goal posts for what is the ideal SAT solver
What is also interesting is their changing ideals. Constantly trying to put a positive spin on their Dynex SAT solver, while clearly contradicting their earlier statements.
From September 2022 onwards the claim of the Dynex SAT solver is that it is the only solver able to solve a specific problem. Even quantum computers could not possibly solve that problem:
Existing methodologies based on current and Quantum technology (reducing the complexity with Shor’s algorithm to O(n⁵⁰,000) cannot solve this problem today as it would require longer than the existence of the universe to find a solution. The Dynex Neuromorphic Chip solves the problem in 2.23s because of its inherent parallelization, it’s long-range order and its capability to utilize instantons.
- Dynex-Neuromorphic-Chip commit 46a8354
They spice that up with this nice benchmark table showing for other solution it takes longer than the universe exists AND longer than the universe exits (sic). Sounds like a really long time:
This was the given and accepted truth for over six months since nobody I guess ran any other SAT solvers on the input outside of what they were referencing to. Just as recently as May 12 2023 they even posted an article titled “Dynex: Testing Efficacy and Performance of DynexSolve Proof-of-Useful-Work (PoUW)” that was highlighting this SAT solver.
After those benchmarks on YalSAT and reported to Dynex there started a flurry of activity on their GitHub account:
According to the commit history this is all activity around the SAT solver benchmarks. As a response to the YalSAT numbers they add a bunch of new data points, most of which the single threaded YalSAT solver does not solve in their defined cap of 15 minutes. There is no doubt this isn’t true.
After the parallel PalSAT numbers come in they do more changes and add the PalSAT results using three threads (instead of the default eight that they used before). With these configurations Dynex SAT is better, but is the mythical configuration there just to make DynexSolve look good? Why do they have 8 threads as a default, if the ideal number is 3? For the record PalSAT handily beats Dynex SAT by being over twice as fast with 8 threads.
Another interesting update in these is the moving of goal posts. Up until last week the claim was that nothing on this earth could solve the problems, except for Dynex SAT. Now suddenly you need to tune the input and solver parameters so that you can beat a solver dating back to 2017? Instead of an incredible achievement it is now a merely a prototype:
In comparison [to PalSAT], the Dynex reference implementation, which has not been optimised for speed but to showcase the calculations in a clear and understandable way in the source code, requires only between 15–183 integration steps to find a solution.
- Dynex-Neuromorphic-Chip commit 463d483
That seems like quite a stark departure from being the only one solving it in ~2 seconds and any other solution in “longer than the universe exists”.
Maybe I don’t understand efficiency?
Additionally before it was imperative that what matters is the speed that it takes to reach the solution. Now instead they take on that TTS is irrelevant (I think its Total Time to Solution?). Instead they’ve unleashed minions to talk about the mathematical elegance and efficiency of their solution. I probably can’t appreciate the elegance of it, but for efficiency I think anyone with some memory of basic high school physics can question that.
In the SAT videos you can see Dynex going full throttle for over two minutes on 9 CPU cores. PalSAT uses a maximum of eight that fluctuate from zero to full load for just under a minute in total. Let’s round those two minutes for Dynex and one for the PalSAT solver for good measure.
The workloads are probably not identical, but the margin in length of the computing time is long enough that we can assume they would fully saturate an 8 core Ryzen like the 5800X. If you run that full on for 1 minute or 2 minutes you can reason that it will use around twice as much energy for the same result. Is that more efficient? Does not sound like that to me.
As always we invite Sumitomo from Dynex to respond to these simple questions on a public forum. Because you tried to remove the Dynex bitcoin talk thread we invite you to write a comment on this article or in the comment for the YouTube video 🎥 below
