Entailing Generalization Boosts Enumeration

Dror Fried, Alexander Nadel, Roberto Sebastiani, Yogev Shalmon

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

תקציר

Given a combinational circuit Γ with a single output o, AllSAT-CT is the problem of enumerating all solutions of Γ. Recently, we introduced several state-of-the-art AllSAT-CT algorithms based on satisfying generalization, which generalizes a given total Boolean solution to a smaller ternary solution that still satisfies the circuit. We implemented them in our open-source tool HALL. In this work we draw upon recent theoretical works suggesting that utilizing generalization algorithms, which can produce solutions that entail the circuit without satisfying it, may enhance enumeration. After considering the theory and adapting it to our needs, we enrich HALL’s AllSAT-CT algorithms by incorporating several newly implemented generalization schemes and additional SAT solvers. By conducting extensive experiments we show that entailing generalization substantially boosts HALL’s performance and quality (where quality corresponds to the number of reported generalized solutions per instance), with the best results achieved by combining satisfying and entailing generalization.

שפה מקוריתאנגלית
כותר פרסום המארח27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024
עורכיםSupratik Chakraborty, Jie-Hong Roland Jiang
מוציא לאורSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
מסת"ב (אלקטרוני)9783959773348
מזהי עצם דיגיטלי (DOIs)
סטטוס פרסוםפורסם - אוג׳ 2024
אירוע27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024 - Pune, הודו
משך הזמן: 21 אוג׳ 202424 אוג׳ 2024

סדרות פרסומים

שםLeibniz International Proceedings in Informatics, LIPIcs
כרך305
ISSN (מודפס)1868-8969

כנס

כנס27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024
מדינה/אזורהודו
עירPune
תקופה21/08/2424/08/24

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

Publisher Copyright:
© Dror Fried, Alexander Nadel, Roberto Sebastiani, and Yogev Shalmon.

טביעת אצבע

להלן מוצגים תחומי המחקר של הפרסום 'Entailing Generalization Boosts Enumeration'. יחד הם יוצרים טביעת אצבע ייחודית.

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