SATIC: An Optimizing Ising Compiler for SAT(isfiability)

Ising machines show great potential as hardware solvers for combinatorial optimization problems such as Boolean Satisfiability (SAT) - one of the hardest classic problems of practical importance. Unlocking this potential, however, is only possible by bridging the gap between SAT problem characteristics and Ising machine specifics. In this paper, we introduce a novel optimizing compiler featuring a bag of powerful heuristic tricks, SATIC, toward this goal. We evaluate SATIC on a representative manufactured Ising chip. Our measurements show that SATIC enables Ising machines to solve up to $\text{73} \times$ larger SAT problems than the hardware capacity would otherwise allow, demonstrating unmatched performance and scalability.