• 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 Sun Apr 14, 2024 11:15:51