양자 어닐러(Quantum annealers)는 에너지 함수가 해밀토니안(Hamiltonian)인 프로그래밍 가능한 물리 시스템인 2-local Ising 모델의 최저 에너지(기저, ground) 상태를 찾음으로써 문제를 해결합니다. 우리는 재귀적 Datalog 프로그램을 이러한 모델로 컴파일하여, 기저 상태가 프로그램의 최소 헤브랜드 모델(minimal Herbrand model)로 투영되도록 합니다. 컴파일러는 이진화(binarization), 그라운딩(grounding), Min-Ones SAT 공식으로의 축소(reduction), 그리고 Ising 인코딩(Ising encoding)의 네 단계를 거칩니다. 각 규칙은 해당 규칙을 위반하는 단 하나의 할당에 대해 에너지 페널티(energy penalty)가 되며, 모든 참인 원자(true atom)에 부여되는 작은 균등 비용(uniform cost)은 최소 모델을 선택합니다. 우리는 단계별 정당성 보조정리(correctness lemmas)와 대응 정리(correspondence theorem)를 통해 이론과 실무 모두에 기여하며, 이는 Lean 4에서 검증되어 컴파일된 모델의 기저 상태가 프로그램의 최소 헤브랜드 모델로 투영됨을 입증합니다. 우리는 컴파일된 모델을 상용 어닐러의 토폴로지(topologies)에 매핑하고, 고전적 및 시뮬레이션된 양자 어닐링(simulated-quantum annealing) 환경에서 해당 인증된 기저 상태가 도달 가능한지, 그리고 언제 도달하는지를 특성화합니다.