Search papers, labs, and topics across Lattice.
This paper presents a method for compiling recursive Datalog programs into 2-local Ising models suitable for quantum annealers, enabling the ground state of the model to correspond to the program's minimal Herbrand model. The compilation process involves four stages: binarization, grounding, reduction to a Min-Ones SAT formula, and Ising encoding, with correctness established through theoretical lemmas and a verified correspondence theorem in Lean 4. The authors also investigate the mapping of these models onto commercial annealer topologies, analyzing conditions under which the certified ground state can be achieved using both classical and simulated-quantum annealing techniques.
Compiling recursive logic programs into quantum annealers could revolutionize how we solve complex computational problems by ensuring optimal solutions are reached efficiently.
Quantum annealers solve problems by finding the lowest-energy (ground) state of a programmable physical system, a 2-local Ising model, whose energy function is the Hamiltonian. We compile recursive Datalog programs into such models so that the ground state projects onto the program's minimal Herbrand model. The compiler has four stages: binarization, grounding, reduction to a Min-Ones SAT formula, and Ising encoding. Each rule becomes an energy penalty on the one assignment that violates it, and a small uniform cost on every true atom selects the minimal model. We contribute both in theory and in practice with per-stage correctness lemmas and a correspondence theorem, verified in Lean 4, establishing that the ground state of the compiled model projects onto the program's minimal Herbrand model. We map the compiled models onto the topologies of commercial annealers and characterize, under classical and simulated-quantum annealing, whether and when that certified ground state is attained.
