University of Limerick
Browse
Heras_2012_empricial.pdf (183.75 kB)

An empirical study of encodings for group MaxSAT ⋆

Download (183.75 kB)
conference contribution
posted on 2013-01-02, 14:25 authored by Federico Heras, Antonio Morgado, Joao Marques-Silva
Weighted Partial MaxSAT (WPMS) is a well-known optimization variant of Boolean Satisfiability (SAT) that finds a wide range of practical applications.WPMS divides the formula in two sets of clauses: The hard clauses that must be satisfied and the soft clauses that can be unsatisfied with a penalty given by their associated weight. However, some applications may require each constraint to be modeled as a set or group of clauses. The resulting formalism is referred to as Group MaxSAT. This paper overviews Group MaxSAT, and shows how several optimization problems can be modeled as Group MaxSAT. Several en- codings from Group MaxSAT to standard MaxSAT are formalized and refined. A comprehensive empirical study compares the performance of several MaxSAT solvers with the proposed encodings. The results indicate that, depending on the underlying MaxSAT solver and problem domain, the solver may perform better with a given encoding than with the others.

History

Publication

The 25th Canadian Conference on Artificial Intelligence (AI2012). Lecture Notes in Computer Science;7310, pp. 85-96

Publisher

Springer

Note

peer-reviewed

Other Funding information

SFI

Rights

The original publication is available at www.springerlink.com

Language

English

Usage metrics

    University of Limerick

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC