Boolean Satisfiability Research Platform

DACROQ implements computational tools for Boolean satisfiability problems in conjunctive normal form. The platform supports comparative analysis of digital and analog solving methodologies.

Solver Implementations

• Digital SAT solvers: Kissat, WalkSAT
• Medusa_0: 28nm GRXO-based mixed-signal solver with distributed clause feedback architecture, RISC-V core integration

Problem Generation

• Forced: k-SAT instances with planted solutions for satisfiable problems
• Unforced: Uniform random k-SAT instances for both satisfiable and unsatisfiable problems