Description:
- Hardware and software verification
-
Logistics
-
Autonomous systems
Abstract
USC researchers have designed a circuit arrangement to accelerate solving of the SAT algorithm. This two-part circuit uses a memory cell to represent values of a Boolean satisfiability expression and a constraints network that modifies the memory cell. The design builds on a previous optimization circuit to produce output voltages that will not exist unless the inputs satisfy the formula. Simulations of hard problems with variable ratios of a > 4 take only 60ns to 3.15us to stabilize, with an extremely fast calculation time of 520ns.
Benefit
Market Application
The Boolean satisfiability (SAT) algorithm plays a crucial role in industries such as hardware and software verification, logistics, and autonomous systems. However, existing SAT algorithms suffer from exponential worst-case complexity, leading to extended product development time or compromised results due to runtime limitations. Consequently, accelerating SAT would enhance hardware and software correctness, reduce time-to-market, and unlock the potential for more advanced autonomous systems. Furthermore, accelerated SAT would have a widespread impact by improving a broad range of fundamental algorithms, given the polynomial complexity transformation from any NP-complete problem to SAT.
Other
Stage of Development