Functional Synthesis via Input-Output Separation

TL;DR

This paper introduces a novel input-output decomposition approach for Boolean functional synthesis, enabling more efficient solutions for complex specifications and complementing existing methods with promising experimental results.

Contribution

The work presents a new decomposition technique based on input-output separation, providing theoretical efficiency improvements and practical effectiveness for challenging synthesis problems.

Findings

Theoretically faster synthesis for specific input component structures.

Experimental results show improved performance on difficult instances.

The method complements existing synthesis algorithms effectively.

Abstract

Boolean functional synthesis is the process of constructing a Boolean function from a Boolean specification that relates input and output variables. Despite significant recent developments in synthesis algorithms, Boolean functional synthesis remains a challenging problem even when state-of-the-art methods are used for decomposing the specification. In this work we bring a fresh decomposition approach, orthogonal to existing methods, that explores the decomposition of the specification into separate input and output components. We make use of an input-output decomposition of a given specification described as a CNF formula, by alternatingly analyzing the separate input and output components. We exploit well-defined properties of these components to ultimately synthesize a solution for the entire specification. We first provide a theoretical result that, for input components with specific structures, synthesis for CNF formulas via this framework can be performed more efficiently than in the general case. We then show by experimental evaluations that our algorithm performs well also in practice on instances which are challenging for existing state-of-the-art tools, serving as a good complement to modern synthesis techniques.