It would seem the Dynex team is watching this space as they've organized an independent crypto youtuber to validate their claims that their SAT solver is real: https://www.youtube.com/watch?v=SkgPwYXCTeY

On the surface this seems like an incredible feat, solving something in minutes than in days (or never). However, their demo solver seems to be an implementation of a parallel local search SAT solver. They have been well researched and operate on a two common techniques; Parallel local search algorithms and the portfolio approach. A few relevant links on the topic:

• https://baldur.iti.kit.edu/theses/ParallelLSSat.pdf
• https://link.springer.com/article/10.1007/s42979-021-00476-0
• https://github.com/arminbiere/yalsat

The last example is a generic SAT implementation that can solve the "transformed_barthel_n_100000_r_8.000_p0_0.080_instance_001.cnf" example problem in 14.32 seconds on a low spec computer, not infinity. With some tuning it should be close to the Dynex implementation.