A Circuit-Level Amoeba-Inspired SAT Solver

TL;DR

This paper introduces CL-AmbSAT, a hardware-efficient, circuit-level SAT solver inspired by biological processes, which outperforms traditional stochastic local search methods in finding solutions with fewer iterations.

Contribution

The paper proposes a novel circuit model for SAT solving that mimics AmbSAT's parallelism, enabling efficient hardware implementation and improved performance over existing solvers.

Findings

CL-AmbSAT finds solutions with fewer iterations than ProbSAT.

CL-AmbSAT outperforms AmbSAT in simulation.

The approach is hardware-friendly and easily implementable.

Abstract

AmbSAT (or AmoebaSAT) is a biologically-inspired stochastic local search (SLS) solver to explore solutions to the Boolean satisfiability problem (SAT). AmbSAT updates multiple variables in parallel at every iteration step, and thus AmbSAT can find solutions with a fewer number of iteration steps than some other conventional SLS solvers for a specific set of SAT instances. However, the parallelism of AmbSAT is not compatible with general-purpose microprocessors in that many clock cycles are required to execute each iteration; thus, AmbSAT requires special hardware that can exploit the parallelism of AmbSAT to quickly find solutions. In this paper, we propose a circuit model (hardware-friendly algorithm) that explores solutions to SAT in a similar way to AmbSAT, which we call circuit-level AmbSAT (CL-AmbSAT). We conducted numerical simulation to evaluate the search performance of CL-AmbSAT for a set of randomly generated SAT instances that was designed to estimate the scalability of our approach. Simulation results showed that CL-AmbSAT finds solutions with a fewer iteration number than a powerful SLS solver, ProbSAT, and outperforms even AmbSAT. Since CL-AmbSAT uses simple combinational logic to update variables, CL-AmbSAT can be easily implemented in various hardware.