תקציר
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.
שפה מקורית | אנגלית |
---|---|
כותר פרסום המארח | 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023 |
עורכים | Meena Mahajan, Friedrich Slivovsky |
מוציא לאור | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
עמודים | 9:1-9:18 |
מספר עמודים | 18 |
מסת"ב (אלקטרוני) | 9783959772860 |
מזהי עצם דיגיטלי (DOIs) | |
סטטוס פרסום | פורסם - אוג׳ 2023 |
אירוע | 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023 - Alghero, איטליה משך הזמן: 4 יולי 2023 → 8 יולי 2023 |
סדרות פרסומים
שם | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
כרך | 271 |
ISSN (מודפס) | 1868-8969 |
כנס
כנס | 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023 |
---|---|
מדינה/אזור | איטליה |
עיר | Alghero |
תקופה | 4/07/23 → 8/07/23 |
הערה ביבליוגרפית
Publisher Copyright:© 2023 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. All rights reserved.