Constraint-Based Synthesis Of Datalog Programs

We study the problem of synthesizing recursive Datalog programs from examples. We propose a constraint-based synthesis approach that uses an SMT solver to efficiently navigate the space of Datalog programs and their corresponding derivation trees. We demonstrate our technique's ability to synthesize a range of graph-manipulating recursive programs from a small number of examples. In addition, we demonstrate our technique's potential for use in automatic construction of program analyses from example programs and desired analysis output.