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, cryptanalysis, 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 both FPGA and ASIC platforms based on CMOS process. The designs were evaluated on a suite of hard SAT benchmark problems with 20 to 250 variables, demonstrating orders-of-magnitude improvements in both speed and energy efficiency over prior CPU-based software solvers. Moreover, the ASIC implemented in 12nm FinFET process and developed using standard digital EDA flow, outperforms state-of-the-art ASIC SAT accelerators in terms of solution time and scalability.