I mean I can actually imagine people trying challenges with NISQ computers down the line.

Grover's quadratic speedup is provably optimal in the black-box setting. We expect general SAT to be essentially unstructured and as hard as the black-box setting (strong exponential time hypothesis). It's believable that Grover is optimal there. But this is not clear for 3-SAT.

Also, thanks to my great collaborators, mxkramer.bsky.social, Alexander Nietner and @jenseisert.bsky.social!

3-SAT is clearly more structured than SAT in general, as evidenced by the improved classical runtime of O(1.307^n) compared to the 2^n for SAT. Using Grover on top of a classical solver, this structure is only addressed classically, inherently capping the achievable speedup at quadratic.

Grover's quadratic speedup is provably optimal in the black-box setting. We expect general SAT to be essentially unstructured and as hard as the black-box setting (strong exponential time hypothesis). It's believable that Grover is optimal there. But this is not clear for 3-SAT.

To be clear: This line of research is not about exponential quantum advantages, but polynomial ones. 3-SAT is an NP-hard problem and is NOT expected to be efficiently solvable on a quantum computer.

To get a worst-case scaling of the form O(c^n), we would need a lower bound on the gap of the SAT instance encoding Hamiltons. Unfortunately, we did not manage this and after talking to a few experts, this seems to be a difficult task. We leave this as an open problem.

Regarding the algorithmic improvements, I particularly like our perfect hash family based scheme for parallelizing local measurements in the algorithm.

Obvious candidate because strong numerical performance is known for this algorithm, but theoretical understanding is limited. We provide an expression for the worst-case runtime depending on the Hamiltonian gap as well as interesting algorithmic improvements.

We look at such an algorithm in scirate.com/arxiv/2511.0..., namely the measurement-driven SAT solver from Benjamin, Zhao and Fitzsimons, which I think is an obvious candidate algorithm for this line of thought.
BZF algorithm: arxiv.org/abs/1711.02687

Here is the referee report for that paper. :) Same would apply here.

Just looked for the code and there is a Julia package, I love that!