From Propositional Model Counting to SAT Solving and Back
Date&Time: 18 October 2019 - h. 9.00
Venue: Via Sommarive 5 - Polo Ferrari 1 (Povo, TN) - Toblino Room
Speaker
- Sibylle Möhle Rotondi - Johannes Kepler University Linz, Austria
Abstract
Exact Propositional model counting has various applications. One major challenge in model counting -and therefore also in model enumeration- is the fact that the search space needs to be examined exhaustively. We addressed this issue by means of a dual approach which enables the determination of partial models [1]. Non-chronological backtracking was considered an important feature of modern SAT solver. However, it also poses particular challenges to model counting. A SAT solver based on chronological backtracking won the main track of the SAT competition 2018. The corresponding paper presented at SAT'18 described the algorithm and provided empirical evidence of its correctness, but a formalization and proofs were missing. We provided a formalization and formal proof of the method as well as a generalization and experimental confirmation of its effectiveness [2]. We finally combined chronological backtracking and CDCL for (non-dual) propositional model counting [3]. This talk will be a collage of the presentations of the three cited papers.
[1] S. Möhle, A. Biere, "Dualizing Projected Model Counting", ICTAI'18
[2] S. Möhle, A. Biere, “Backing Backtracking”, SAT’19
[3] S. Möhle, A. Biere, “Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting”, GCAI’19
About the Speaker
Sibylle Möhle obtained her diploma in Computer Science with minor Medical Informatics from the FernUniversität in Hagen (Germany), which is a distance education university, in 2014. From 2015 to 2018 she was employed as a research assistant working towards a PhD at TU Dresden, before in 2018 she joined the Institute for Formal Models and Verification led by Armin Biere at Johannes Kepler University Linz as a PhD student.
Contact: roberto.sebastiani [at] unitn.it (Roberto Sebastiani )