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: |