HiM: An Autonomous Hardware Accelerator for Solving Boolean Satisfiability Problem with a Heuristic-in-Macro Engine

Boolean Satisfiability (SAT), an NP-complete problem central to EDA and AI, has motivated hardware acceleration to overcome its exponential complexity. Early approaches focused on speeding up incomplete solvers, but their inherent algorithmic limitations made them unsuitable for correctness-critical tasks. Consequently, the focus shifted to hardware accelerators for complete solvers based on the DPLL/CDCL framework, which concentrated on accelerating the primary bottleneck: the Boolean Constraint Propagation (BCP) operation. However, performance is ultimately dominated by branching heuristics. Existing designs either omit heuristics, suffering large penalties, or offload them to CPUs, incurring prohibitive overhead. This work presents Heuristic-in-Macro (HiM), the first fully autonomous SAT accelerator integrating both an efficient BCP engine and a hardware-embedded MOMs branching heuristic in a single macro, eliminating CPU dependence. A high-throughput parallel processing architecture replaces traditional serialized clause scans with a tiled multi-macro execution, achieving 8.78× acceleration. At the circuit level, physical efficiency is enhanced through a compact 16T unit cell that merges logic and storage, thereby reducing area and energy. Proposed HiM-based solver achieves 100% SAT/UNSAT solvability, 172.1× speedup in algorithmic performance compared to designs without heuristics. When matched against a CPU-offloaded hybrid system, HiM is 305.6× faster and 1.99×106× more energy-efficient. Compared to the widely used MiniSAT software solver, HiM delivers 26.7× speedup and 3.09×106× efficiency, while reducing time- and energy-to-solution by up to 94% and 83% versus state-of-the-art ASIC accelerators.