A PN-Free Digital 3-SAT Accelerator Using Crossbar Architecture and Frequency-Controlled Counters

Boolean satisfiability (SAT) solving is a foundational problem in computer science and serves as a core engine for a wide range of combinatorial optimization tasks. It underpins critical applications across formal verification, electronic design automation (EDA), artificial intelligence (AI) reasoning, crypt-analysis, bioinformatics, and constraint programming. While significant progress has been made in algorithmic improvements, these advances are gradually reaching saturation, motivating increasing attention toward domain-specific hardware accelerators beyond the von Neumann architecture. However, existing hardware SAT accelerators often face significant deployment barriers due to reliance on pseudo-random number (PN) generators, specialized analog components with sufficient intrinsic noise, or unconventional fabrication technologies such as memristors. These limitations hinder scalability, portability, and integration into mainstream digital design flows. This paper presents an intrinsically stochastic, fully digital SAT accelerator inspired by analog mixed-signal crossbar architectures. The proposed design eliminates the need for analog noise sources, PN generators, or true-random number (TN) generators, enabling a fully synthesizable, standard-cell-based implementation compatible with conventional digital flows. Digital counters are employed as “spins”, acting as oscillatory elements that store and flip variable states, thus supporting robust and scalable stochastic behavior. Stochasticity is achieved through a novel polynomial clause-to-variable feedback mechanism, which dynamically modulates oscillator frequencies based on clause satisfaction states, allowing effective exploration of the solution space without external randomness. A highly parallel crossbar structure further accelerates problem-solving by enabling concurrent evaluation of multiple clauses, aided by a proposed polynomial clause-to-variable feedback function. To validate the proposed architecture, we implemented prototypes on FPGA and three ASIC platforms including 12 nm FinFET, 22 nm and 65 nm CMOS technologies. The designs were evaluated on a suite of hard SAT benchmark problems with 20 to 250 variables. Our 22nm ASIC accelerator achieves an approximately$3.06 \times$speedup than the state-of-the-art 28 nm 3-SAT accelerator. Compared with prior 65 nm designs, ours achieves 100% solvability with comparable runtime. Notably, we present the first 3-SAT accelerator capable of handling 250 variables with 100% solvability, marking a significant advancement in scalability for digital SAT accelerators.