Daedalus 3-SAT solver
DAEDALUS is a mixed-signal chip that searches for solutions to 3-SAT problems with up to 50 variables. It represents variables with oscillators and uses feedback from unsatisfied clauses to change their states.
Architecture
Each variable maps to a relaxation oscillator, and each clause is evaluated by a three-input NOR gate. Analog and digital crossbars connect the variables and clauses, allowing any variable to appear in any clause within the chip's capacity.
Feedback
Oscillators change state only while receiving feedback from unsatisfied clauses. Once every clause is satisfied, that feedback stops and the circuit holds its solution. This removes the need to sample a continuously changing state.
Measurements
The chip was tested on the 1,000-instance SATLIB sets for 20 and 50 variables, with 100 runs per instance. It solved every instance in those sets. Mean solution times were 1.6 µs for 20-variable problems and 31.7 µs for 50-variable problems. The solver occupies 0.58 mm².
The papers above include the full test conditions and comparisons with WalkSAT.