M. J. Kramer, P. Boes, J. Eisert (2026)
Using deep learning to construct stochastic local search SAT solvers with performance bounds

Published in Mach. Learn.: Sci. Technol. 7 025057

Preprint arXiv:2309.11452

GitHub Repository

Abstract: 

The Boolean Satisfiability problem (SAT), as the prototypical NP-complete problem, is crucial in both theoretical computer science and practical applications. To address this problem, stochastic local search (SLS) algorithms, which iteratively and randomly update candidate assignments, present an important and theoretically well-studied class of solvers. Recent theoretical advancements have identified conditions under which SLS solvers efficiently solve SAT instances, provided they have access to suitable "oracles", i.e., instance-specific distribution samples. We propose leveraging machine learning models, particularly graph neural networks (GNN), as oracles to enhance the performance of SLS solvers. Our approach, evaluated on random and pseudo-industrial SAT instances, demonstrates a significant performance improvement regarding step counts and solved instances. Our work bridges theoretical results and practical applications, highlighting the potential of purpose-trained SAT solvers with performance guarantees.

M. J. Kramer, C. Schubert, J. Eisert (2026)
A measurement-driven quantum algorithm for SAT: Performance guarantees via spectral gaps and measurement parallelization
Preprint arXiv:2603.04540

LinkedIn post

Abstract:

We establish tight inapproximability bounds for max-LINSAT, the problem of maximizing the number of satisfied linear constraints over the finite field 𝔽q, where each constraint accepts r values. Specifically, we prove by a direct reduction from Håstad's theorem that no polynomial-time algorithm can exceed the random-assignment ratio r/q by any constant, assuming 𝖯≠𝖭𝖯. This threshold coincides with the ℓ/m→0 limit of the semicircle law governing decoded quantum interferometry (DQI), where ℓ is the decoding radius of the underlying code: as the decodable structure vanishes, DQI's approximation ratio degrades to exactly the worst-case bound established by our result. Together, these observations delineate the boundary between worst-case hardness and potential quantum advantage, showing that any algorithm surpassing r/q must exploit structure specific to the instance.

F. J. Schreiber*, M. J. Kramer*, A. Nietner, J. Eisert (2025)
A measurement-driven quantum algorithm for SAT: Performance guarantees via spectral gaps and measurement parallelization

(* = equal contribution)

Preprint arXiv:2511.09647

LinkedIn post

This work was accepted as a talk at QCTiP 2026 in Oxford

Abstract:

The Boolean satisfiability problem (SAT) is of central importance in both theory and practice. Yet, most provable guarantees for quantum algorithms rely exclusively on Grover-type methods that cap the possible advantage at only quadratic speed-ups, making the search for approaches that surpass this quadratic barrier a key challenge. In this light, this work presents a rigorous worst-case runtime analysis of a recently introduced measurement-driven quantum SAT solver. Importantly, this quantum algorithm does not exclusively rely on Grover-type methods and shows promising numerical performance. Our analysis establishes that the algorithm's runtime depends on an exponential trade-off between two key properties: the spectral gap of the associated Hamiltonian and the success probability of the driving measurements. We show that this trade-off can be systematically controlled by a tunable rotation angle. Beyond establishing a worst-case runtime expression, this work contributes significant algorithmic improvements. First, we develop a new readout routine that efficiently finds a solution even for instances with multiple satisfying assignments. Second, a measurement parallelization scheme, based on perfect hash families, is introduced. Third, we establish an amplitude-amplified version of the measurement-driven algorithm. Finally, we demonstrate the practical utility of our framework: By suitably scheduling the algorithm's parameters, we show that its runtime collapses from exponential to polynomial on a special class of SAT instances, consistent with their known classical tractability. A problem we leave open is to establish a non-trivial lower bound on the spectral gap as a function of the rotation angle. Resolving this directly translates into an improved worst-case runtime, potentially realizing a super-quadratic quantum advantage.

M. J. Kramer (2023)
On Quantum Algorithms for Satisfiability Problems

I submitted this work as my Master's thesis. Prof. Dr. Jens Eisert, Alexander Nietner, Paul K. Fährmann, and Johannes Jakob Meyer supervised this project. The full text is available on request.

Abstract:

In this work, we look at quantum algorithms from the perspective of classical optimization. We acknowledge that optimization problems that are classically hard in worst-case complexity can surely be solved in polynomial time for large classes of instances. In this work, we focus on satisfiability problems.

For example, in a Boolean satisfiability problem (SAT), if the clauses have a limited dependency on each other, one can find solutions in polynomial time using the Moser-Tardos algorithm. This can be rigorously explained using the Lovász Local Lemma. We study the classical background and also contribute here: We present a project where we use the Lovász Local Lemma and deep learning to construct stochastic local search solvers for SAT with performance guarantees. This is done by training an oracle factory, which can be used in the Moser-Tardos algorithm. We see that the machine-learning-boosted version of the Moser-Tardos algorithm can solve significantly more random 3-SAT instances than its uniform version. In addition, it is much faster regarding the steps it needs. Furthermore, we pitch an idea to study the relation of the Moser-Tardos algorithm to simulated annealing algorithms.

The main focus of this manuscript is to apply ideas from the classical side on the quantum side. Here, we try to find quantum algorithms that take inspiration from the Moser-Tardos algorithm. Luckily, the Lovász Local Lemma extends to the quantum setting. Therefore, it can be used to get a guarantee that certain instances of the quantum satisfiability problem (QSAT) are satisfiable. Those instances that fulfill the quantum generalization of the Lovász Local Lemma are studied, and we look at quantum algorithms that are guaranteed to find a satisfying state on those instances efficiently. We review the literature and propose a novel quantum algorithm that numerically outperforms existing quantum algorithms by orders of magnitude. We report various numerical results. Furthermore, we try to prove and understand the fast convergence of our algorithm analytically. Various ideas and attempts are presented. In particular, we show a proof of convergence to the ground state for our algorithm. In addition, we numerically study the behavior of our algorithm on random 3-QSAT instances. The performance beyond the regime where the Quantum Lovász Local Lemma guarantees satisfiability is reported.

M. J. Kramer (2021)
A Variational Approach for Quantum Annealing within the LHZ Architecture

I submitted this work as my Bachelor's thesis. Prof. Dr. Wolfgang Lechner, Dr. Andreas Hartmann, and Prof. Dr. Tilman Enss supervised this project. The full text is available on request.

Abstract:

In this thesis, I present an overview of adiabatic quantum computing and quantum annealing. I focus on the Lechner-Hauke-Zoller (LHZ) architecture proposed for an Ising model. This architecture is scalable, fully connected, and can be implemented using local interactions only. The main focus of this thesis is a variational approach within the LHZ architecture recently proposed by Susa and Nishimori. The schedule function for the constraint term that occurs in the LHZ architecture via construction is variationally improved during several diabatic sweeps. It is observed for a ferromagnetic Ising model and for spin-glass samples that the variationally obtained non-monotonic schedule function increases the final ground-state fidelity significantly.
Furthermore the obtained energy expectation value decreases towards the true ground state energy. In this thesis, I implemented an LHZ architecture in Python and reproduced the numerical results presented by Susa and Nishimori. Furthermore, my numerical studies go into a bit more into detail. Namely, I varied some more free parameters.