2026-07-20T15:08:03Z https://drops.dagstuhl.de/oai

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

Hierarchical Stochastic SAT and Quality Assessment of Logic Locking Scholl, Christoph Seufert, Tobias Siegwolf, Fabian Stochastic Boolean Satisfiability Hierarchical Stochastic SAT Binary Decision Diagrams Decision Procedure Motivated by the application of quality assessment of logic locking we introduce Hierarchical Stochastic SAT (HSSAT) which generalizes Stochastic SAT (SSAT). We look into the complexity of HSSAT and for solving HSSAT formulas we provide a prototype solver which computes exact evaluation results (i.e., without any approximation and without any imprecision caused by numerical rounding errors). Finally, we perform an intensive experimental evaluation of our HSSAT solver in the context of quality assessment of logic locking. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christoph Scholl and Tobias Seufert and Fabian Siegwolf 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.24 urn:nbn:de:0030-drops-205462 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.24 eng https://creativecommons.org/licenses/by/4.0/legalcode