PBCounter: weighted model counting on pseudo-boolean formulas

doi:10.1007/s11704-024-3631-1

Front. Comput. Sci.

2025, Vol. 19

Issue (3) : 193402 https://doi.org/10.1007/s11704-024-3631-1

Theoretical Computer Science

PBCounter: weighted model counting on pseudo-boolean formulas

Yong LAI^1,², Zhenghang XU^1,², Minghao YIN^2,³(

)

¹. College of Computer Science and Technology, Jilin University, Changchun 130012, China
². Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education, Jilin University, Changchun 130012, China
³. School of Computer Science and Information Technology, Northeast Normal University, Changchun 130017, China

Download: PDF(3907 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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 $P B C o u n t e r$ . We compare $P B C o u n t e 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 $P B C o u n t e r$ is superior to the model counters on CNF formulas.

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

Corresponding Author(s): Minghao YIN

Just Accepted Date: 19 January 2024 Issue Date: 14 May 2024

Cite this article:

Yong LAI,Zhenghang XU,Minghao YIN. PBCounter: weighted model counting on pseudo-boolean formulas[J]. Front. Comput. Sci., 2025, 19(3): 193402.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-024-3631-1
https://academic.hep.com.cn/fcs/EN/Y2025/V19/I3/193402

Fig.1 The five possible ADDs of

2 x 1 + 3 x 2 ≥ b

over

x 1 ? x 2

Benchmark(#)	NoPre	OnlyBb	$P B C o u n t e r$
PB06 (287)	28	37	39
ExactCover (539)	192	193	194
WSN (600)	387	425	483
Total (1426)	607	655	716

Tab.1 Results of different preprocessing techniques

Solvers	Instances solved
Solvers	Unique	Fastest	Total
VBS1(with $P B C o u n t e r$ )	?	?	750
VBS0(without $P B C o u n t e r$ )	?	?	557
$P B C o u n t e r$	110	327	716
$P B C o u n t e r$ _NoPre	19	62	607
SharpSAT-TD + Warners	3	11	531
SharpSAT-TD + ArcCons	0	2	520
ExactMC + Warners	0	3	511
ExactMC + ArcCons	0	327	499
D4 + Warners	0	0	445
D4 + ArcCons	1	18	480
ADDMC + Warners	0	0	155
ADDMC + ArcCons	0	0	266

Tab.2 The number of instances solved by solvers

Fig.2 A cactus plot of the numbers of benchmarks solved by ten weighted model counters and two virtual best solvers (VBS1, with

P B C o u n t e r

, and VBS0, without

P B C o u n t e r

)

Benchmark (#)	$P B C o u n t e r$	RSBlock	IntCount
PB06 (287)	39	16	5
ExactCover (539)	194	178	8
WSN (600)	483	0	23
Total (1426)	716	194	36

Tab.3 Results of different approaches

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	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

[1]

FCS-23631-OF-YL_suppl_1

Download

Viewed

Full text

Abstract

Cited

Shared

Discussed