Medusa k-SAT solver
MEDUSA is a mixed-signal chip for solving Boolean satisfiability (SAT) problems: finding values that satisfy a set of logical constraints. It supports up to 200 variables and 1,016 clauses, using a network of oscillators to search for a solution.
Architecture
The chip contains two compute tiles, each with 200 oscillator cells and 508 programmable clause cells, and a RISC-V digital supervisor. The clause cells can be configured for different SAT problems without changing the hardware.
How it works
Each Boolean variable is represented by an oscillator. Unsatisfied clauses send feedback that changes the oscillator states. Make and break feedback accounts for both clauses that need to be satisfied and clauses that would become unsatisfied if a variable changed. Digital links couple the tiles so they can work on the same problem.
Measurements
For the 50-variable, 218-clause SATLIB benchmark (uf50-218), mean time to solution was 4.92 µs and mean energy to solution was 19.1 nJ. The chip occupies 2.59 mm², with 1.29 mm² per tile. The papers above describe the benchmarks and comparisons.