BAXMC: a CEGAR approach to Max#SAT

TL;DR

This paper introduces BAXMC, a CEGAR-based algorithm for Max#SAT that leverages exact or approximate model counting, demonstrating significantly improved efficiency over existing methods.

Contribution

It presents a novel CEGAR approach for Max#SAT with proven correctness and enhanced performance, applicable to formulas with existential quantifiers.

Findings

Algorithm outperforms state-of-the-art methods in efficiency

Proven correctness for both exact and approximate model counting

Effective complexity is significantly improved

Abstract

Max#SAT is an important problem with multiple applications in security and program synthesis that is proven hard to solve. It is defined as: given a parameterized quantifier-free propositional formula compute parameters such that the number of models of the formula is maximal. As an extension, the formula can include an existential prefix. We propose a CEGAR-based algorithm and refinements thereof, based on either exact or approximate model counting, and prove its correctness in both cases. Our experiments show that this algorithm has much better effective complexity than the state of the art.