Dual Approach to Solving SAT in Hardware

Boolean Satisfiability (SAT) is a central problem appearing in artificial intelligence, logic reasoning, formal verification, and EDA, with a wide range of practical applications. Many efficient SAT solvers have been implemented in software using some version of the DPLL algorithm. Numerous attempts have been made to implement SAT solving in hardware. However, all known hardware SAT solvers basically mimic the DPLL-like software approach, and are typically implemented as hardware accelerators that support the decision engine implemented in software. Herein, we propose a drastically different way to solve the SAT problem in a reconfigurable hardware. The basic idea is to convert (on the fly) the problem specified in the traditional CNF form to a disjunctive normal form (DNF), but stop the conversion as soon as the first nonzero product of literals in the DNF has been found. The paper describes the basic approach, the required hardware architecture, and demonstrates its potential for solving large SAT problems. Initial experimental results based on a simple prototype are encouraging, showing several orders of magnitude speedup w.r.t. software solutions.