@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@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.
  },
}