论文标题
BAXMC：最大＃SAT的CEGAR方法
BAXMC: a CEGAR approach to Max#SAT
论文作者
论文摘要
Max＃SAT是一个重要的问题，具有多个安全性和程序合成中的应用程序，很难解决。它被定义为：给定无参数化量词的命题公式计算参数，以使公式的模型数量最大。作为扩展，该公式可以包括存在前缀。我们根据精确的模型计数提出了一种基于CEGAR的算法及其改进，并在两种情况下都证明了其正确性。我们的实验表明，该算法的有效复杂性比最新的状态更好。
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.
