Addressing Proposition Model Counting and Enumeration with and without Projection
Sprache des Vortragstitels:
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 . In our second approach, we combine non-chronological backtracking and CDCL . 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 , 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 . This talk will be a collage of the cited papers.
 S. Möhle, A. Biere, "Dualizing Projected Model Counting", ICTAI'18
 S. Möhle, A. Biere, ?Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting?, GCAI?19
 S. Möhle, A. Biere, ?Backing Backtracking?, SAT?19
 S. Möhle, R. Sebastiani, A. Biere, "Four Flavors of Entailment", SAT'20