Anzeige
Erschienen in:
2015 | OriginalPaper | Buchkapitel
Exploiting Resolution-Based Representations for MaxSAT Solving
verfasst von : Miguel Neves, Ruben Martins, Mikoláš Janota, Inês Lynce, Vasco Manquinho
Erschienen in: Theory and Applications of Satisfiability Testing -- SAT 2015
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Most recent MaxSAT algorithms rely on a succession of calls to a SAT solver in order to find an optimal solution. In particular, several algorithms take advantage of the ability of SAT solvers to identify unsatisfiable subformulas. Usually, these MaxSAT algorithms perform better when small unsatisfiable subformulas are found in early iterations of the algorithm. However, this is not the case in many problem instances, since the whole formula is given to the SAT solver in each call.
In this paper, we propose to partition the MaxSAT formula using a resolution-based graph representation. Partitions are then iteratively joined by using a proximity measure extracted from the graph representation of the formula. The algorithm ends when only one partition remains and the optimal solution is found. Experimental results show that this new approach further enhances a state of the art MaxSAT solver to optimally solve a larger set of industrial problem instances.