Although state-of-the-art (SOTA) SAT solvers based on conflict-driven clause learning (CDCL) have achieved remarkable engineering success, their sequential nature limits the parallelism that may be extracted for acceleration on platforms such as the graphics processing unit (GPU). In this work, we propose FastFourierSAT, a highly parallel hybrid SAT solver based on gradient-driven continuous local search (CLS). This is achieved by a parallel algorithm inspired by the fast Fourier transform (FFT)-based convolution for computing the elementary symmetric polynomials (ESPs), which is the major computational task in previous CLS methods. The complexity of our algorithm matches the best previous result. Furthermore, the substantial parallelism inherent in our algorithm can leverage the GPU for acceleration, demonstrating significant improvement over the previous CLS approaches. FastFourierSAT is compared with a wide set of SOTA parallel SAT solvers on extensive benchmarks including combinatorial and industrial problems. Results show that FastFourierSAT computes the gradient 100+ times faster than previous prototypes on CPU. Moreover, FastFourierSAT solves most instances and demonstrates promising performance on larger-size instances.

This paper presents a novel Pseudo-Boolean Optimization (PBO) framework to solve the Rectilinear Steiner Minimum Arborescence (RSMA) problem, with a focus on the All-Quadrant RSMA scenario. Our framework is designed to compute exact solutions efficiently, even in the presence of isothetic rectilinear obstacles. We also introduce a reduction technique that can reduce more than 17% of the encoded variables and constraints to improve solving efficiency. Our method guarantees optimality and offers flexibility and adaptability for large-scale instances. The experimental results indicate that the proposed framework solves 82.3% of 40-point instances and 64.3% of 50-point instances within 300 seconds.

Memristive crossbars have been proposed as a promising pathway to enabling all-to-all connections for a variety of applications. One such application is the latch-based dynamical Ising machine, which have been proposed for solving combinatorial optimization problems. However, the impact of the design of the memristive crossbar on the performance of the latch-based Ising machine remains unclear. We present a SPICE-level model and simulation framework for analyzing and evaluating the latch-based dynamical Ising machine that use memristive crossbars to achieve all-to-all coupling between Ising spins implemented as latches. Our design space exploration reveals that the solution quality is highly sensitive to the circuit and device design parameters and sizes of the problems. An effective metric that can capture the effect of several design parameters on the statistical results is then proposed to quantify the system functionality. Finally, optimization techniques based on our proposed metric that models the effect of several design parameters on the solution quality of the Ising machine are proposed and demonstrated on MaxCut solving. Our evaluation results on a 128×128 crossbar array-based design show >98% solution quality across a wide range of problem sizes is achievable.