Gaussian Elimination Meets Maximum Satisfiability

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.