Symbolic Functional Decomposition: A Reconfiguration Approach

TL;DR

This work introduces a symbolic framework for functional decomposition and reconfiguration of Boolean functions, representing factor functions with OBDDs, the reconfiguration via a Boolean circuit, and the target function class with a second-order finite automaton. It proves fixed-parameter tractable linear-time algorithms for functional reconfiguration and decomposition with key parameters being the OBDD width $p$, circuit size $m$, the number of factors $k$, and $|\mathcal{A}|$, including a concrete bound $2^{p^{O(2^m)}}\cdot |\mathcal{A}|^k \cdot |D|$. The authors develop an automata-theoretic toolkit—relations as languages, selectors, and width-aware constructions—that yields regularity results and enables efficient composition of factor functions under width constraints. Applications include generalized juntas and OBDD factorization, demonstrating practical utility in modular function synthesis and circuit design. The framework also suggests connections to learning with queries and potential oracle-based generalizations, offering a principled, parameterized approach to decomposition under reconfiguration constraints.

Abstract

Functional decomposition is the process of breaking down a function $f$ into a composition $f=g(f_1,\dots,f_k)$ of simpler functions $f_1,\dots,f_k$ belonging to some class $\mathcal{F}$. This fundamental notion can be used to model applications arising in a wide variety of contexts, ranging from machine learning to formal language theory. In this work, we study functional decomposition by leveraging on the notion of functional reconfiguration. In this setting, constraints are imposed not only on the factor functions $f_1,\dots,f_k$ but also on the intermediate functions arising during the composition process. We introduce a symbolic framework to address functional reconfiguration and decomposition problems. In our framework, functions arising during the reconfiguration process are represented symbolically, using ordered binary decision diagrams (OBDDs). The function $g$ used to specify the reconfiguration process is represented by a Boolean circuit $C$. Finally, the function class $\mathcal{F}$ is represented by a second-order finite automaton $\mathcal{A}$. Our main result states that functional reconfiguration, and hence functional decomposition, can be solved in fixed-parameter linear time when parameterized by the width of the input OBDD, by structural parameters associated with the reconfiguration circuit $C$, and by the size of the second-order finite automaton $\mathcal{A}$.

Figures (1)

• Figure 1: An OBDD of width $2$ and length $4$ accepting all strings in $\{0,1\}^4$ of odd parity. Note that each string of odd parity (say, $1011$) reaches the element $1$ in the image of the last layer, while each string of even parity (say, $1010$) reaches the element $0$ in the image of the last layer.

Theorems & Definitions (41)

• definition 1
• theorem 2: bryant1992symbolicMeloOliveira2022
• proposition 1
• proof
• definition 2
• theorem 3: MeloOliveira2022
• definition 3: Reconfiguration Width
• theorem 4
• lemma 1
• proof