• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Engineering an Efficient PB-XOR Solver.
Jiong Yang, and Kuldeep S. Meel.
In Proceedings of International Conference on Constraint Programming (CP), September 2021.
Model counting is a fundamental problem in computer science with a wide range of applications such as quantitatively property verification, probabilistic reasoning, and network reliability. Given a formula F, the problem of model counting is to compute the number of solutions of F. The formula F can be a CNF or Pseudo-Boolean (PB) formula or any other form. In the past few years, we have witnessed the rise of hashing-based approximate model counting over CNF formulas on top of CNF-XOR solving. For lack of PB-XOR solving techniques, for the PB formula, the existing approach trivially encodes PB constraints into CNF and applies CNF counting technique, which fails to utilize more powerful pseudo-Boolean reasoning.In this paper, we handle PB-XOR solving and present the first approximate model counter over pseudo-Boolean constraints to leverage the power of PB reasoning based on recent improvements in PB solving. We engineer an efficient counter named ApproxMC-PB, equipping PB solver RoundingSat with Gauss-Jordan-Elimination-based tactics to bridge the gap between PB and XOR constraints. Extensive experiments on quantitative verification of binarized neural network properties reveal that ApproxMC-PB significantly outperforms state-of-the-art counters on pseudo-Boolean benchmarks, and there is ample room for optimizing the interaction between PB and XOR constraints.
@inproceedings{YM21, title={Engineering an Efficient PB-XOR Solver}, author={Yang, Jiong and Meel, Kuldeep S.}, booktitle=CP, month=sep, year={2021}, bib2html_rescat={Solver Engineering}, bib2html_dl_pdf={../Papers/cp21-ym.pdf}, bib2html_pubtype={Refereed Conference}, abstract={Model counting is a fundamental problem in computer science with a wide range of applications such as quantitatively property verification, probabilistic reasoning, and network reliability. Given a formula F, the problem of model counting is to compute the number of solutions of F. The formula F can be a CNF or Pseudo-Boolean (PB) formula or any other form. In the past few years, we have witnessed the rise of hashing-based approximate model counting over CNF formulas on top of CNF-XOR solving. For lack of PB-XOR solving techniques, for the PB formula, the existing approach trivially encodes PB constraints into CNF and applies CNF counting technique, which fails to utilize more powerful pseudo-Boolean reasoning. In this paper, we handle PB-XOR solving and present the first approximate model counter over pseudo-Boolean constraints to leverage the power of PB reasoning based on recent improvements in PB solving. We engineer an efficient counter named ApproxMC-PB, equipping PB solver RoundingSat with Gauss-Jordan-Elimination-based tactics to bridge the gap between PB and XOR constraints. Extensive experiments on quantitative verification of binarized neural network properties reveal that ApproxMC-PB significantly outperforms state-of-the-art counters on pseudo-Boolean benchmarks, and there is ample room for optimizing the interaction between PB and XOR constraints.}, }
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Thu Aug 22, 2024 18:37:34