What's hard about Boolean Functional Synthesis

TL;DR

This paper explores the inherent complexity of Boolean functional synthesis, proving exponential lower bounds, and introduces a two-phase algorithm that performs efficiently on most benchmarks despite worst-case exponential complexity.

Contribution

The paper demonstrates the exponential hardness of Boolean functional synthesis and proposes a practical two-phase algorithm that outperforms existing methods on many benchmarks.

Findings

First phase is efficient and often produces correct solutions

A sufficient condition guarantees the correctness of the first phase

Experimental results show superior performance over state-of-the-art techniques

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 a majority of benchmarks.