@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{SM21,
  title={Gaussian Elimination meets Maximum Satisfiability},
  author={Soos, Mate and Meel, Kuldeep S.},
  booktitle=KR,
  year={2021},
  month=nov,
  bib2html_rescat={Solver Engineering},
  bib2html_pubtype={Refereed Conference},
  bib2html_dl_pdf={../Papers/kr21-sm.pdf},
  abstract={
    Given a set of constraints F and a weight function W over the assignments,
    the problem of MaxSAT is to compute a maximum weighted solution of $F$.
    MaxSAT is a fundamental problem with applications in numerous areas. The
    success of MaxSAT solvers has prompted researchers in AI and formal methods
    communities to develop algorithms that can use MaxSAT solver as oracle. One
    such problem that stands to benefit from advances in MaxSAT solving is
    discrete integration. Recently, Ermon et al. achieved a significant
    breakthrough by reducing the problem of integration to polynomially many
    queries to an optimization oracle where $F$ is conjuncted with randomly
    chosen XOR constraints. Unlike approximate model counting, where
    hashing-based approaches have been able to achieve scalability as well as
    rigorous formal guarantees, the practical evaluation of Ermon et al's
    approach, called WISH, often sacrifice theoretical guarantees, largely due
    to lack of existing MaxSAT solvers with native XOR support.
    The primary contribution of this paper is a new MaxSAT solver, GaussMaxHS,
    with built-in XOR support. The architecture of GaussMaxHS is inspired by
    CryptoMiniSAT, which has been the workhorse of hashing-based approximate
    model counting techniques. The resulting solver, GaussMaxHS, outperforms
    MaxHS over 9628 benchmarks arising from spin glass models and network
    reliability domains. In particular, with a timeout of 5000 seconds, MaxHS
    could solve only 5473 benchmarks while GaussMaxHS could solve 6120
    benchmarks.
  },
}