License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2023.9
URN: urn:nbn:de:0030-drops-184717
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18471/
Fried, Dror ;
Nadel, Alexander ;
Shalmon, Yogev
AllSAT for Combinational Circuits
Abstract
Motivated by the need to improve the scalability of Intel’s in-house Static Timing Analysis (STA) tool, we consider the problem of enumerating all the solutions of a single-output combinational Boolean circuit, called AllSAT-CT. While AllSAT-CT is immediately reducible to enumerating the solutions of a Boolean formula in Conjunctive Normal Form (AllSAT-CNF), our experiments had shown that such a reduction, followed by applying state-of-the-art AllSAT-CNF tools, does not scale well on neither our industrial AllSAT-CT instances nor generic circuits, both when the user requires the solutions to be disjoint or when they can be non-disjoint. We focused on understanding the reasons for this phenomenon for the well-known iterative blocking family of AllSAT-CNF algorithms. We realized that existing blocking AllSAT-CNF algorithms fail to generalize efficiently for AllSAT-CT, since they are restricted to Boolean logic. Consequently, we introduce three dedicated AllSAT-CT algorithms that are ternary-logic-aware: a ternary simulation-based algorithm TALE, a dual-rail&MaxSAT-based algorithm MARS, and their combination. Specifically, we introduce in MARS two novel blocking clause generation approaches for the disjoint and non-disjoint cases. We implemented our algorithms in our new tool HALL. We show that HALL scales substantially better than any reduction to existing AllSAT-CNF tools on our industrial STA instances as well as on publicly available families of combinational circuits for both the disjoint and the non-disjoint cases.
BibTeX - Entry
@InProceedings{fried_et_al:LIPIcs.SAT.2023.9,
author = {Fried, Dror and Nadel, Alexander and Shalmon, Yogev},
title = {{AllSAT for Combinational Circuits}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {9:1--9:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18471},
URN = {urn:nbn:de:0030-drops-184717},
doi = {10.4230/LIPIcs.SAT.2023.9},
annote = {Keywords: AllSAT, SAT, Circuits}
}
