Compiling Logic Programs for Quantum Annealers

Researchers at University of Tartu and colleagues present a novel method for solving complex computational problems using quantum annealers. They demonstrate a compilation process that transforms recursive Datalog programs into 2-local Ising models, enabling the annealer to find solutions corresponding to the program’s minimal Herbrand model. This work advances the field by providing both theoretical guarantees, including correctness lemmas and a correspondence theorem formally verified in Lean 4, and practical implementation, mapping compiled models onto existing quantum annealing hardware. The team characterised whether and when the certified ground state is attained through both classical and simulated-quantum annealing, representing a significant step towards utilising quantum annealers for logic programming tasks.

Recursive Datalog programs are now compiled into models suitable for quantum annealers by Bruno Rucy Carneiro Alves de Lima and colleagues at Tartu and Lucidarium Systems. This compilation yields 2-local Ising models, enabling the minimal Herbrand model of the program to be found using quantum annealing.

The compilation utilises a four-stage process and incorporates a single uniform cost applied to every true atom within the Datalog program. A new compilation method translates complex logic programs into a format suitable for quantum annealers, enabling these specialised computers to solve a broader range of knowledge-based problems, specifically recursive Datalog programs, than previously possible.

The team rigorously verified the process, ensuring the quantum annealer’s solution accurately reflects the intended meaning of the original logic program using formal methods. This compilation process transforms recursive Datalog programs, a set of rules that define relationships and can refer back to themselves, into a 2-local Ising model.

A 2-local Ising model is akin to a network of switches that can be flipped to find the lowest energy state, representing the solution. The team verified this translation, ensuring the quantum annealer’s solution accurately reflects the original program’s meaning, and are now exploring whether this certified ground state can be reliably attained.

Minimal energy cost enables reliable Datalog to Ising model compilation and verification

A key reduction in the energy cost of unfounded atoms was achieved, decreasing it to just one ε per atom, where ε represents a small uniform cost. This threshold allows the compiled model to reliably distinguish between correct and incorrect solutions, a feat previously unattainable with larger costs that obscured the minimal model within the energy field. Refined cost structure, alongside formal verification in Lean 4, ensures the ground state of the compiled 2-local Ising model accurately projects onto the minimal Herbrand model of the recursive Datalog program.

Verification of the compilation process occurred across several recursive Datalog programs, including ‘tc_path’ and ‘tc_cycle’, establishing that the resulting 2-local Ising models project onto the program’s minimal Herbrand model. Detailed energy field analysis of the ‘nonlinear_tc_path’ program, comprising 19 ground atoms and 524,288 possible assignments, revealed a unique global minimum and only 18 single-flip local minima. The addition of unfounded atoms increased energy by one unit each.

Experiments compiling these models onto D-Wave’s Pegasus and Zephyr topologies mapped 31 logical spins to a median of 34 physical qubits. The compiler comprises four stages: binarization, grounding, reduction to a Min-Ones SAT formula, and Ising encoding, each preserving the minimal Herbrand model. These results confirm the theoretical correspondence between the logical program and the physical annealer, but currently focus on small instances and do not yet demonstrate scalability to the larger, more complex problems required for practical application.

Accurate translation of logic programs to quantum annealers validates a new computational approach

A method to translate complex logic programs into a format compatible with quantum annealers has been devised, opening doors to solving a wider range of knowledge-based problems. The compilation process, which includes binarization, grounding, reduction to Min-Ones SAT, and Ising encoding, establishes a direct link between logical rules and the physical properties of the annealer. Lean 4 theorem prover verified the correctness of each stage, ensuring the quantum solution accurately reflects the original program’s meaning.

While rigorous verification ensured the quantum annealer’s solution accurately reflects the original logic, a key limitation remains unaddressed. Current work focuses on verifying feasibility, not speed, and acknowledging the absence of a demonstrated speed advantage over conventional methods is important.

The research successfully translated recursive Datalog programs into a 2-local Ising model suitable for quantum annealers, and verified that the lowest-energy state of this model corresponds to the program’s logical solution. This demonstrates a method for representing knowledge-based problems in a way that quantum hardware can process, offering a new avenue for computation.

Researchers verified the correctness of each translation stage using the Lean 4 theorem prover, and mapped logical spins onto D-Wave topologies with a median of 34 physical qubits. The study focused on establishing this correspondence and does not yet address scalability or speed advantages over existing methods.