2026-07-21T14:19:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18471 2024-03-06T11:01:59Z ddc:004 open_access

AllSAT for Combinational Circuits Fried, Dror Nadel, Alexander Shalmon, Yogev AllSAT SAT Circuits 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dror Fried and Alexander Nadel and Yogev Shalmon 2023 Is Part Of LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2023.9 urn:nbn:de:0030-drops-184717 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.9 eng https://creativecommons.org/licenses/by/4.0/legalcode