|
|
||
|
IMADA -Department of Mathematics and Computer Science |
|
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 applications in symbolic quantitative AI, including its relation to Bayesian inference. We briefly overview solving techniques and explain a parameterized algorithm and implementation to tackle the problem. While purely parameterized approaches from theory often suffer practical limitations, we illustrate that a parameterized algorithm can be successful when combining it with modern hardware that takes advantage of parallelism. Host: Fabrizio Montesi SDU HOME | IMADA HOME Daniel Merkle |