Racket#lang Karp: Formulating and Random Testing NP Reductions
Reduction, a pervasive idea in computer science, is often taught in algorithm courses with NP problems. The traditional pen-and-paper approach is notoriously ineffective both for students and instructors: Subtle mistakes in reductions are often hard to detect by merely inspecting the purported solutions. Constructing a counterexample by hand to expose the mistake is even more onerous. Based on the observation that reductions are actually programs, we designed #lang Karp, a DSL for formulating and random testing NP reductions.
In this presentation, Chenhao Zhang discusses the implementation of Karp on top of Racket and solver-aided host language Rosette.
Watch now: presentation