A Data-Driven Approach for Skolem Function Synthesis


Synthesizing Skolem functions is one of the challenging problems in Computer Science. It has seen multiple proposals, including incremental determination, decomposition techniques from knowledgecompilation, and counterexample guided refinement techniques via self-substitutions. In this work, we propose a novel data-driven approach to synthesis that employs constrained sampling techniques for generation of data, machine learning for candidate Skolem functions, and automated reasoning to verify and refine to generate Skolem functions. Our approach achieves significant performance improvements by solving 63/609 benchmarks that could not be solved by any of the existing synthesis tools.

LiVe 2020: 4th Workshop on Learning in Verification