We address the problem of constructing a solver for a certain search problem from its solution verifier. The main idea behind the approach we advocate is to consider a verifier as an interpreter which takes a data structure to search in as a program and a candidate solution as this program’s input. As a result the interpreter returns “true” if the candidate solution satisfies all constraints and “false” otherwise. Being implemented in a relational language, a verifier becomes capable of finding a solution as well. We apply two techniques to make this scenario realistic: relational conversion and supercompilation. Relational conversion makes it possible to convert a first-order functional program into relational form, while supercompilation (in the form of conjunctive partial deduction (CPD)) — to optimize out redundant computations. We demonstrate our approach on a number of examples using a prototype tool for OCanren — an implementation of miniKanren for OCaml, — and discuss the results of evaluation.