Program Synthesis and Descriptive Complexity

Lukasz Kaiser

Descriptive complexity theory teaches that many complexity classes have natural logical characterisations. We investigate how this knowledge can be exploited for automatic synthesis of programs from these classes and reductions between them. In particular, quantifier-free formulas are sufficient for reductions between most well-known complete problems. We implemented a program that automatically looks for such reductions by reducing the problem to a one-alternation QBF instance and exploiting propositional solvers. We compare how different solvers perform on this task and report which reductions can be found and which remain out of reach for this technique at present.