FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
What’s hard about Boolean Functional Synthesis?

Authors: S. Akshay, Supratik Chakraborty, Shubham Goel, Sumith Kulal and Shetal Shah

Paper Information

Title:What’s hard about Boolean Functional Synthesis?
Authors:S. Akshay, Supratik Chakraborty, Shubham Goel, Sumith Kulal and Shetal Shah
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:Boolean Functional synthesis, Skolem functions, Approximate synthesis, Computational Hardness
Abstract:

ABSTRACT. Given a relational specification between Boolean inputs and outputs, the goal of Boolean functional synthesis is to synthesize each output as a function of the inputs such that the specification is met. In this paper, we first show that unless some hard conjectures in complexity theory are falsified, Boolean functional synthesis must necessarily generate exponential-sized Skolem functions, thereby requiring exponential time, in the worst-case. Given this inherent hardness, what does one do to solve the problem? We present a two-phase algorithm for Boolean functional synthesis, where the first phase is efficient both in terms of time and sizes of synthesized functions, and solves an overwhelming majority of benchmarks. To explain this surprisingly good performance, we provide a sufficient condition under which the first phase must produce exact correct answers. When this condition fails, the second phase builds upon the result of the first phase, possibly requiring exponential time and generating exponential-sized functions in the worst-case. Detailed experimental evaluation shows our algorithm to perform better than state-of-the-art techniques for the vast majority of benchmarks.

Pages:19
Talk:Jul 14 16:00 (Session 99A: Synthesis)
Paper: