AllSAT for Combinational Circuits

Dror Fried, Alexander Nadel, Yogev Shalmon

פרסום מחקרי: פרק בספר / בדוח / בכנספרסום בספר כנסביקורת עמיתים

תקציר

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 יולי 20238 יולי 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/238/07/23

הערה ביבליוגרפית

Publisher Copyright:
© 2023 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. All rights reserved.

טביעת אצבע

להלן מוצגים תחומי המחקר של הפרסום 'AllSAT for Combinational Circuits'. יחד הם יוצרים טביעת אצבע ייחודית.

פורמט ציטוט ביבליוגרפי