PBCounter: weighted model counting on pseudo-boolean formulas
Yong LAI1,2, Zhenghang XU1,2, Minghao YIN2,3()
1. College of Computer Science and Technology, Jilin University, Changchun 130012, China 2. Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education, Jilin University, Changchun 130012, China 3. School of Computer Science and Information Technology, Northeast Normal University, Changchun 130017, China
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 . We compare 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 is superior to the model counters on CNF formulas.
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
L, Duenas-Osorio K S, Meel R, Paredes M Y Vardi . 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
D Roth . On the hardness of approximate reasoning. Artificial Intelligence, 1996, 82(1−2): 273−302
5
T, Sang P, Beame H Kautz . Performing Bayesian inference by weighted model counting. In: Proceedings of the 20th National Conference on Artificial Intelligence. 2005, 475−481
6
M, Chavira A Darwiche . On probabilistic inference by weighted model counting. Artificial Intelligence, 2008, 172(6−7): 772−799
7
C, Domshlak J Hoffmann . Probabilistic planning via heuristic forward search and weighted model counting. Journal of Artificial Intelligence Research, 2007, 30: 565–620
8
Den Broeck G, Van D Suciu . Query processing on probabilistic data: a survey. Foundations and Trends® in Databases, 2017, 7(3−4): 197−341
9
D, Fierens Den Broeck G, Van J, Renkens D, Shterionov B, Gutmann I, Thon G, Janssens L D Raedt . Inference and learning in probabilistic logic programs using weighted Boolean formulas. Theory and Practice of Logic Programming, 2015, 15( 3): 358–401
10
Y, Lai K S, Meel R H C Yap . The power of literal equivalence in model counting. In: Proceedings of the AAAI Conference on Artificial Intelligence. 2021, 3851−3859
11
T, Sang F, Bacchus P, Beame H, Kautz T Pitassi . 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
M Thurley . 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
S, Sharma S, Roy M, Soos K S Meel . GANAK: a scalable probabilistic exact model counter. In: Proceedings of the 28th International Joint Conference on Artificial Intelligence. 2019, 1169−1176
14
J M, Lagniez P Marquis . An improved decision-DNNF compiler. In: Proceedings of the 26th International Joint Conference on Artificial Intelligence. 2017, 667−673
15
J, Dudek V, Phan M Vardi . ADDMC: weighted model counting with algebraic decision diagrams. In: Proceedings of the AAAI Conference on Artificial Intelligence. 2020, 1468−1476
16
M, Hecher P, Thier S Woltran . 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
S, Chakraborty K S, Meel M Y Vardi . A scalable approximate model counter. In: Proceedings of the 19th International Conference on Principles and Practice of Constraint Programing. 2013, 200−216
19
Y, Lai K S, Meel R H C Yap . Fast converging anytime model counting. In: Proceedings of the AAAI Conference on Artificial Intelligence. 2023, 4025−4034
20
Berre D, Le P, Marquis S, Mengel R Wallon . 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
F A, Aloul A, Ramani I L, Markov K A Sakallah . 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
Z, Lei S, Cai C, Luo H Hoos . 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
F A, Aloul A, Ramani I L, Markov K A Sakallah . 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
H M, Sheini K A Sakallah . Pueblo: a hybrid pseudo-Boolean SAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 2006, 2(1−4): 165−189
26
J, Elffers J Nordström . Divide and conquer: towards faster pseudo-Boolean solving. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence. 2018, 1291−1299
27
Y, Chu S, Cai C, Luo Z, Lei C Peng . 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
W, Zhou Y, Zhao Y, Wang S, Cai S, Wang X, Wang M Yin . 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
A, Huang L, Lloyd M, Omar J Boerkoel . New perspectives on flexibility in simple temporal planning. In: Proceedings of the International Conference on Automated Planning and Scheduling. 2018, 123−131
30
K, Luckow C S, Păsăreanu M B, Dwyer A, Filieri W Visser . 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
C, Ge F, Ma X, Ma F, Zhang P, Huang J Zhang . 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
C, Ge A Biere . Decomposition strategies to count integer solutions over linear constraints. In: Proceedings of the 30th International Joint Conference on Artificial Intelligence. 2021, 1389−1395
33
P G, Kolaitis M Y Vardi . Conjunctive-query containment and constraint satisfaction. Journal of Computer and System Sciences, 2000, 61( 2): 302–332
34
G, Pan M Y Vardi . Symbolic techniques in satisfiability solving. Journal of Automated Reasoning, 2005, 35(1−3): 25−50
35
N, Eén N Sörensson . Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2006, 2(1−4): 1−26
36
A, Aavani D G, Mitchell E Ternovska . New encoding for translating pseudo-Boolean constraints into SAT. In: Proceedings of the 10th Symposium on Abstraction, Reformulation, and Approximation. 2013
37
M, Bofill J, Coll P, Nightingale J, Suy F, Ulrich-Oltean M Villaret . SAT encodings for pseudo-Boolean constraints together with at-most-one constraints. Artificial Intelligence, 2022, 302: 103604
38
R I, Bahar E A, Frohm C M, Gaona G D, Hachtel E, Macii A, Pardo F Somenzi . Algebric decision diagrams and their applications. Formal Methods in System Design, 1997, 10(2−3): 171−206
39
R E, Tarjan M Yannakakis . 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
A M C A, Koster H L, Bodlaender Hoesel S P M Van . Treewidth: computational experiments. Electronic Notes in Discrete Mathematics, 2001, 8: 54–57
41
I, Abío R, Nieuwenhuis A, Oliveras E, Rodríguez-Carbonell V Mayer-Eichberger . A new look at BDDs for pseudo-Boolean constraints. Journal of Artificial Intelligence Research, 2012, 45( 1): 443–480
42
T, Korhonen M Järvisalo . 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
J M, Lagniez E, Lonca P Marquis . Definability for model counting. Artificial Intelligence, 2020, 281: 103229
45
Dijk T, Van De Pol J Van . Sylvan: multi-core framework for decision diagrams. International Journal on Software Tools for Technology Transfer, 2017, 19( 6): 675–696
46
J P Warners . A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 1998, 68( 2): 63–69
47
O, Bailleux Y, Boufkhad O Roussel . A translation of pseudo-Boolean constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2006, 2(1−4): 191−200
48
A, Morgado P J, Matos V, Manquinho J Marques-Silva . Counting models in integer domains. In: Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing. 2006, 410−423
49
T, Junttila P Kaski . 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
S, Verdoolaege R, Seghir K, Beyls V, Loechner M Bruynooghe . 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
M, Soos K S Meel . 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
