2026-07-21T19:24:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20535 2024-08-19T06:03:42Z ddc:004 open_access

Entailing Generalization Boosts Enumeration Fried, Dror Nadel, Alexander Sebastiani, Roberto Shalmon, Yogev Generalization Minimization Prime Implicant AllSAT SAT Circuits 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dror Fried and Alexander Nadel and Roberto Sebastiani and Yogev Shalmon 2024 Is Part Of LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2024.13 urn:nbn:de:0030-drops-205351 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.13 eng https://creativecommons.org/licenses/by/4.0/legalcode