BAXMC: a CEGAR approach to Max#SAT
Logic in Computer Science
2023-02-07 v2
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.
Keywords
Cite
@article{arxiv.2211.00973,
title = {BAXMC: a CEGAR approach to Max#SAT},
author = {Thomas Vigouroux and Cristian Ene and David Monniaux and Laurent Mounier and Marie-Laure Potet},
journal= {arXiv preprint arXiv:2211.00973},
year = {2023}
}
Comments
FMCAD 2022, Oct 2022, Trente, Italy