Addressing Proposition Model Counting and Enumeration with and without Projection
Sprache des Vortragstitels:
Englisch
Original Kurzfassung:
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)
Sprache der Kurzfassung:
Englisch
Vortragstyp:
Andere Vorträge und Präsentationen
Vortragsdatum:
16.07.2020
Vortragsort:
Österreich
Details zum Vortragsort:
online aufgrund von COVID-19 (geplant: DEU, Ludwig-Maximilians-Universität München)