• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Gaussian Elimination meets Maximum Satisfiability.
Mate Soos, and Kuldeep S. Meel.
In Proceedings of International Conference on Knowledge Representation and Reasoning (KR), November 2021.
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.
@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.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Thu Apr 30, 2026 09:22:03