From Propositional Model Counting to SAT Solving and Back
Sprache des Vortragstitels:
Englisch
Original Kurzfassung:
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
Sprache der Kurzfassung:
Englisch
Englischer Vortragstitel:
From Propositional Model Counting to SAT Solving and Back