SAT-Based Complete Don't-Care Computation for Network Optimization

TL;DR

This paper introduces an improved SAT-based method for computing complete don't-cares in Boolean network optimization, enhancing efficiency, robustness, and scalability over previous BDD-based approaches.

Contribution

It proposes the use of complete don't-cares instead of CODCs, implements windowing for large networks, and develops a more efficient SAT-based algorithm.

Findings

Complete don't-cares reduce literals compared to CODCs.

Windowing enables handling of very large networks.

SAT-based computation is faster and more robust than BDD-based methods.

Abstract

This paper describes an improved approach to Boolean network optimization using internal don't-cares. The improvements concern the type of don't-cares computed, their scope, and the computation method. Instead of the traditionally used compatible observability don't-cares (CODCs), we introduce and justify the use of complete don't-cares (CDC). To ensure the robustness of the don't-care computation for very large industrial networks, a optional windowing scheme is implemented that computes substantial subsets of the CDCs in reasonable time. Finally, we give a SAT-based don't-care computation algorithm that is more efficient than BDD-based algorithms. Experimental results confirm that these improvements work well in practice. Complete don't-cares allow for a reduction in the number of literals compared to the CODCs. Windowing guarantees robustness, even for very large benchmarks on which previous methods could not be applied. SAT reduces the runtime and enhances robustness, making don't-cares affordable for a variety of other Boolean methods applied to the network.