QBF-Based Boolean Function Bi-Decomposition

TL;DR

This paper introduces a novel QBF-based method for Boolean function bi-decomposition, achieving optimal partitions with improved quality and demonstrating practical feasibility through experimental validation.

Contribution

It presents the first use of QBF for bi-decomposition, providing optimal solutions that outperform heuristic and BDD-based methods.

Findings

QBF-based bi-decomposition yields more optimal partitions.

Experimental results show improved decomposition quality.

The approach is practically feasible on benchmark problems.

Abstract

Boolean function bi-decomposition is ubiquitous in logic synthesis. It entails the decomposition of a Boolean function using two-input simple logic gates. Existing solutions for bi-decomposition are often based on BDDs and, more recently, on Boolean Satisfiability. In addition, the partition of the input set of variables is either assumed, or heuristic solutions are considered for finding good partitions. In contrast to earlier work, this paper proposes the use of Quantified Boolean Formulas (QBF) for computing bi- decompositions. These bi-decompositions are optimal in terms of the achieved disjointness and balancedness of the input set of variables. Experimental results, obtained on representative benchmarks, demonstrate clear improvements in the quality of computed decompositions, but also the practical feasibility of QBF-based bi-decomposition.