תקציר
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 אוג׳ 2024 → 24 אוג׳ 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/24 → 24/08/24 |
הערה ביבליוגרפית
Publisher Copyright:© Dror Fried, Alexander Nadel, Roberto Sebastiani, and Yogev Shalmon.