TY - JOUR
AU - Lagniez, Jean-Marie
AU - Marquis, Pierre
PY - 2019/07/17
Y2 - 2024/07/19
TI - A Recursive Algorithm for Projected Model Counting
JF - Proceedings of the AAAI Conference on Artificial Intelligence
JA - AAAI
VL - 33
IS - 01
SE - AAAI Technical Track: Constraint Satisfaction and Optimization
DO - 10.1609/aaai.v33i01.33011536
UR - https://ojs.aaai.org/index.php/AAAI/article/view/3967
SP - 1536-1543
AB - <p>We present a recursive algorithm for projected model counting, i.e., the problem consisting in determining the number of models k∃<em>X.</em>Σk of a propositional formula Σ after eliminating from it a given set <em>X</em> of variables. Based on a ”standard” model counter, our algorithm projMC takes advantage of a disjunctive decomposition scheme of ∃<em>X.</em>Σ for computing k∃<em>X.</em>Σk. It also looks for disjoint components in its input for improving the computation. Our experiments show that in many cases projMC is significantly more efficient than the previous algorithms for projected model counting from the literature.</p>
ER -