Addressing Proposition Model Counting and Enumeration with and without Projection

Description

Model counting and model enumeration are key tasks in various activities. One major challenge is the fact that the search space needs to be examined exhaustively. In this seminar, I present the different approaches we pursued in addressing this issue. The first one is a dual approach based on CDCL, which enables the determination of partial models under projection [1]. In our second approach, we combine non-chronological backtracking and CDCL [2]. Non-chronological backtracking was considered an important feature of CDCL-based SAT solvers. However, it also poses particular challenges to model counting, since found models need be blocked to prevent multiple counts resulting in a potential blowup of the formula. This blowup can be avoided by backtracking chronologically, but results in the violation of several invariants considered crucial for CDCL. A fix to this problem was presented at SAT'18. We formalized and generalized this method and provided a proof of its correctness [3], laying the foundation for our second approach. We recently proposed a completely different method making use of chronological backtracking and dual reasoning inspired by how theory and SAT solvers interact in lazy Satisfiability Modulo Theories [4]. This talk will be a collage of the cited papers. [1] S. Möhle, A. Biere, "Dualizing Projected Model Counting", ICTAI'18 (http://fmv.jku.at/papers/MoehleBiere-ICTAI18.pdf) [2] S. Möhle, A. Biere, “Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting”, GCAI’19 (http://fmv.jku.at/papers/MoehleBiere-GCAI19.pdf) [3] S. Möhle, A. Biere, “Backing Backtracking”, SAT’19 (http://fmv.jku.at/papers/MoehleBiere-SAT19.pdf) [4] S. Möhle, R. Sebastiani, A. Biere, "Four Flavors of Entailment", SAT'20 (https://link.springer.com/content/pdf/10.1007%2F978-3-030-51825-7_5.pdf)

Period	16 Jul 2020
Event title	unbekannt/unknown
Event type	Other
Location	AustriaShow on map