PBCounter: weighted model counting on pseudo-boolean formulas

Abstract

In Weighted Model Counting (WMC), we assign weights to literals and compute the sum of the weights of the models of a given propositional formula where the weight of an assignment is the product of the weights of its literals. The current WMC solvers work on Conjunctive Normal Form (CNF) formulas. However, CNF is not a natural representation for human-being in many applications. Motivated by the stronger expressive power of Pseudo-Boolean (PB) formulas than CNF, we propose to perform WMC on PB formulas. Based on a recent dynamic programming algorithm framework called ADDMC for WMC, we implement a weighted PB counting tool \mathsf{P}\mathsf{B}\mathsf{C}\mathsf{o}\mathsf{u}\mathsf{n}\mathsf{t}\mathsf{e}\mathsf{r}. We compare \mathsf{P}\mathsf{B}\mathsf{C}\mathsf{o}\mathsf{u}\mathsf{n}\mathsf{t}\mathsf{e}\mathsf{r} with the state-of-the-art weighted model counters SharpSAT-TD, ExactMC, D4, and ADDMC, where the latter tools work on CNF with encoding methods that convert PB constraints into a CNF formula. The experiments on three domains of benchmarks show that \mathsf{P}\mathsf{B}\mathsf{C}\mathsf{o}\mathsf{u}\mathsf{n}\mathsf{t}\mathsf{e}\mathsf{r} is superior to the model counters on CNF formulas.

Graphical abstract

Keywords

weighted model counting / pseudo-boolean constraint / algebraic decision diagrams / preprocessing techniques

References

[1] Baluta T, Shen S, Shinde S, Meel K S, Saxena P. Quantitative verification of neural networks and its security applications. In: Proceedings of 2019 ACM SIGSAC Conference on Computer and Communications Security. 2019, 1249−1264

[2] Duenas-Osorio L, Meel K S, Paredes R, Vardi M Y. Counting-based reliability estimation for power-transmission grids. In: Proceedings of the AAAI Conference on Artificial Intelligence. 2017, 4488−4494

[3] Palash Sashittal, and Mohammed El-Kebir SharpTNl: counting and sampling parsimonious transmission networks under a weak bottleneck. RECOMB Comparative Genomics(RECOMB-CG), Montpellier, France, October 1−4, 2019

[4] Roth D. On the hardness of approximate reasoning. Artificial Intelligence, 1996, 82(1−2): 273−302

[5] Sang T, Beame P, Kautz H. Performing Bayesian inference by weighted model counting. In: Proceedings of the 20th National Conference on Artificial Intelligence. 2005, 475−481

[6] Chavira M, Darwiche A. On probabilistic inference by weighted model counting. Artificial Intelligence, 2008, 172(6−7): 772−799

[7] Domshlak C, Hoffmann J . Probabilistic planning via heuristic forward search and weighted model counting. Journal of Artificial Intelligence Research, 2007, 30: 565–620

[8] Van Den Broeck G, Suciu D. Query processing on probabilistic data: a survey. Foundations and Trends® in Databases, 2017, 7(3−4): 197−341

[9] Fierens D, Van Den Broeck G, Renkens J, Shterionov D, Gutmann B, Thon I, Janssens G, Raedt L D . Inference and learning in probabilistic logic programs using weighted Boolean formulas. Theory and Practice of Logic Programming, 2015, 15( 3): 358–401

[10] Lai Y, Meel K S, Yap R H C. The power of literal equivalence in model counting. In: Proceedings of the AAAI Conference on Artificial Intelligence. 2021, 3851−3859

[11] Sang T, Bacchus F, Beame P, Kautz H, Pitassi T. Combining component caching and clause learning for effective model counting. In: Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing. 2004, 1−9

[12] Thurley M. sharpSAT - counting models with advanced component caching and implicit BCP. In: Proceedings of the 9th International Conference Theory and Applications of Satisfiability Testing. 2006, 424−429

[13] Sharma S, Roy S, Soos M, Meel K S. GANAK: a scalable probabilistic exact model counter. In: Proceedings of the 28th International Joint Conference on Artificial Intelligence. 2019, 1169−1176

[14] Lagniez J M, Marquis P. An improved decision-DNNF compiler. In: Proceedings of the 26th International Joint Conference on Artificial Intelligence. 2017, 667−673

[15] Dudek J, Phan V, Vardi M. ADDMC: weighted model counting with algebraic decision diagrams. In: Proceedings of the AAAI Conference on Artificial Intelligence. 2020, 1468−1476

[16] Hecher M, Thier P, Woltran S. Taming high treewidth with abstraction, nested dynamic programming, and database technology. In: Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing. 2020, 343−360

[17] Ermon S, Gomes C, Selman B. Uniform solution sampling using a constraint solver as an oracle. In: Proceedings of the 28th Conference on Uncertainty in Artificial Intelligence. 2012, 255−264

[18] Chakraborty S, Meel K S, Vardi M Y. A scalable approximate model counter. In: Proceedings of the 19th International Conference on Principles and Practice of Constraint Programing. 2013, 200−216

[19] Lai Y, Meel K S, Yap R H C. Fast converging anytime model counting. In: Proceedings of the AAAI Conference on Artificial Intelligence. 2023, 4025−4034

[20] Le Berre D, Marquis P, Mengel S, Wallon R. Pseudo-Boolean constraints from a knowledge representation perspective. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence. 2018, 1891−1897

[21] Kovásznai G, Erdélyi B, Biró C. Investigations of graph properties in terms of wireless sensor network optimization. In: Proceedings of 2018 IEEE International Conference on Future IoT Technologies (Future IoT). 2018, 1−8

[22] Aloul F A, Ramani A, Markov I L, Sakallah K A. Generic ILP versus specialized 0-1 ILP: an update. In: Proceedings of the IEEE/ACM International Conference on Computer Aided Design. 2002, 450−457

[23] Lei Z, Cai S, Luo C, Hoos H. Efficient local search for pseudo Boolean optimization. In: Proceedings of the 24th International Conference on Theory and Applications of Satisfiability Testing. 2021, 332−348

[24] Aloul F A, Ramani A, Markov I L, Sakallah K A. PBS: a backtrack-search pseudo-Boolean solver and optimizer. In: Proceedings of the 5th International Symposium on Theory and Applications of Satisfiability Testing. 2000, 346−353

[25] Sheini H M, Sakallah K A. Pueblo: a hybrid pseudo-Boolean SAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 2006, 2(1−4): 165−189

[26] Elffers J, Nordström J. Divide and conquer: towards faster pseudo-Boolean solving. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence. 2018, 1291−1299

[27] Chu Y, Cai S, Luo C, Lei Z, Peng C. Towards more efficient local search for pseudo-Boolean optimization. In: Proceedings of the 29th International Conference on Principles and Practice of Constraint Programming. 2023, 12

[28] Zhou W, Zhao Y, Wang Y, Cai S, Wang S, Wang X, Yin M. Improving local search for pseudo Boolean optimization by fragile scoring function and deep optimization. In: Proceedings of the 29th International Conference on Principles and Practice of Constraint Programming. 2023, 41

[29] Huang A, Lloyd L, Omar M, Boerkoel J. New perspectives on flexibility in simple temporal planning. In: Proceedings of the International Conference on Automated Planning and Scheduling. 2018, 123−131

[30] Luckow K, Păsăreanu C S, Dwyer M B, Filieri A, Visser W. Exact and approximate probabilistic symbolic execution for nondeterministic programs. In: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering. 2014, 575−586

[31] Ge C, Ma F, Ma X, Zhang F, Huang P, Zhang J. Approximating integer solution counting via space quantification for linear constraints. In: Proceedings of the 28th International Joint Conference on Artificial Intelligence. 2019, 1697−1703

[32] Ge C, Biere A. Decomposition strategies to count integer solutions over linear constraints. In: Proceedings of the 30th International Joint Conference on Artificial Intelligence. 2021, 1389−1395

[33] Kolaitis P G, Vardi M Y . Conjunctive-query containment and constraint satisfaction. Journal of Computer and System Sciences, 2000, 61( 2): 302–332

[34] Pan G, Vardi M Y. Symbolic techniques in satisfiability solving. Journal of Automated Reasoning, 2005, 35(1−3): 25−50

[35] Eén N, Sörensson N. Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2006, 2(1−4): 1−26

[36] Aavani A, Mitchell D G, Ternovska E. New encoding for translating pseudo-Boolean constraints into SAT. In: Proceedings of the 10th Symposium on Abstraction, Reformulation, and Approximation. 2013

[37] Bofill M, Coll J, Nightingale P, Suy J, Ulrich-Oltean F, Villaret M . SAT encodings for pseudo-Boolean constraints together with at-most-one constraints. Artificial Intelligence, 2022, 302: 103604

[38] Bahar R I, Frohm E A, Gaona C M, Hachtel G D, Macii E, Pardo A, Somenzi F. Algebric decision diagrams and their applications. Formal Methods in System Design, 1997, 10(2−3): 171−206

[39] Tarjan R E, Yannakakis M . Simple linear-time algorithms to test chordality of graphs, test acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs. SIAM Journal on Computing, 1984, 13( 3): 566–579

[40] Koster A M C A, Bodlaender H L, Van Hoesel S P M . Treewidth: computational experiments. Electronic Notes in Discrete Mathematics, 2001, 8: 54–57

[41] Abío I, Nieuwenhuis R, Oliveras A, Rodríguez-Carbonell E, Mayer-Eichberger V . A new look at BDDs for pseudo-Boolean constraints. Journal of Artificial Intelligence Research, 2012, 45( 1): 443–480

[42] Korhonen T, Järvisalo M. Integrating tree decompositions into decision heuristics of propositional model counters (short paper). In: Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming. 2021, 8

[43] Lagniez J M, Marquis P. Preprocessing for propositional model counting. In: Proceedings of the 28th AAAI Conference on Artificial Intelligence. 2014, 2688−2694

[44] Lagniez J M, Lonca E, Marquis P . Definability for model counting. Artificial Intelligence, 2020, 281: 103229

[45] Van Dijk T, Van De Pol J . Sylvan: multi-core framework for decision diagrams. International Journal on Software Tools for Technology Transfer, 2017, 19( 6): 675–696

[46] Warners J P . A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 1998, 68( 2): 63–69

[47] Bailleux O, Boufkhad Y, Roussel O. A translation of pseudo-Boolean constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2006, 2(1−4): 191−200

[48] Morgado A, Matos P J, Manquinho V, Marques-Silva J. Counting models in integer domains. In: Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing. 2006, 410−423

[49] Junttila T, Kaski P. Exact cover via satisfiability: an empirical study. In: Proceedings of the 16th International Conference on Principles and Practice of Constraint Programming. 2010, 297−304

[50] Verdoolaege S, Seghir R, Beyls K, Loechner V, Bruynooghe M . Counting integer points in parametric polytopes using Barvinok’s rational functions. Algorithmica, 2007, 48( 1): 37–66

[51] Lagniez J M, Lonca E, Marquis P. Improving model counting by leveraging definability. In: Proceedings of the 25th International Joint Conference on Artificial Intelligence. 2016, 751−757

[52] Soos M, Meel K S. Arjun: an efficient independent support computation technique and its applications to counting and sampling. In: Proceedings of the 41st IEEE/ACM International Conference on Computer Aided Design. 2022, 1−9

RIGHTS & PERMISSIONS

Higher Education Press