A Glimpse into Propositional Model Counting
From International Center for Computational Logic
A Glimpse into Propositional Model Counting
Talk by Johannes K. Fichte
- Location: Online
- Start: 7. July 2022 at 11:00 am
- End: 7. July 2022 at 12:00 pm
- Event series: Research Seminar Logic and AI
- iCal
Model counting (#SAT) asks to compute the number of satisfying assignments for a propositional formula. The decision version (SAT) received widespread interest in computational complexity, formed many applications in modern combinatorial problem solving, and can be solved effectively for millions of variables on structured instances. #SAT is much harder than SAT and requires more elaborate solving techniques. In this talk, we revisit the problem, its complexity, and explain its connection to quantitative AI. We briefly overview solving techniques and illustrate a parameterized algorithm and implementation to tackle the problem. While purely parameterized approaches from theory often suffer practical limitations, we elaborate that a parameterized algorithm can be successful when combining it with modern hardware that takes advantage of parallelism.
