Abstract
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 encodings 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.
This work was partially supported by SFI PI grant BEACON (09/IN.1/I2618).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aksoy, L., Costa, E., Flores, P.F., Monteiro, J.: Exact and approximate algorithms for the optimization of area and delay in multiple constant multiplications. IEEE Trans. on CAD of Integrated Circuits and Systems 27(6) (2008)
Ansótegui, C., Bonet, M.L., Levy, J.: Solving (Weighted) Partial MaxSAT through Satisfiability Testing. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 427–440. Springer, Heidelberg (2009)
Argelich, J., Cabiscol, A., Lynce, I., Manyà, F.: Modelling Max-CSP as Partial Max-SAT. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 1–14. Springer, Heidelberg (2008)
Argelich, J., Manyà, F.: Exact Max-SAT solvers for over-constrained problems. Journal of Heuristics 12(4-5), 375–392 (2006)
Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. JSAT 7, 59–64 (2010)
Biere, A., Heule, M., Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability (2009)
Een, N., Sörensson, N.: Translating Pseudo-Boolean Constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2, 1–26 (2006)
Heras, F., Larrosa, J., Givry, S., Schiex, T.: 2006 and 2007 Max-SAT evaluations: Contributed instances. Journal on Satisfiability, Boolean Modeling and Computation 4(2-4), 239–250 (2008)
Heras, F., Larrosa, J., Oliveras, A.: MiniMaxSat: An efficient weighted Max-SAT solver. Journal of Artificial Intelligence Research 31, 1–32 (2008)
Heras, F., Morgado, A., Marques-Silva, J.: Core-guided binary search for maximum satisfiability. In: AAAI Conference on Artificial Intelligence. AAAI (2011)
Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: ACM Conference on PLDI, pp. 437–446 (2011)
Kautz, H.A., Ruan, Y., Achlioptas, D., Gomes, C.P., Selman, B., Stickel, M.E.: Balance and filtering in structured satisfiable problems. In: IJCAI (2001)
Larrosa, J., Schiex, T.: Solving weighted CSP by maintaining arc consistency. Artif. Intell. 159(1-2), 1–26 (2004)
Maloberti, J., Sebag, M.: Fast theta-subsumption with constraint satisfaction algorithms. Machine Learning 55(2), 137–174 (2004)
Manquinho, V., Martins, R., Lynce, I.: Improving Unsatisfiability-Based Algorithms for Boolean Optimization. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 181–193. Springer, Heidelberg (2010)
Walsh, T.: SAT v CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, pp. 441–456. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Heras, F., Morgado, A., Marques-Silva, J. (2012). An Empirical Study of Encodings for Group MaxSAT. In: Kosseim, L., Inkpen, D. (eds) Advances in Artificial Intelligence. Canadian AI 2012. Lecture Notes in Computer Science(), vol 7310. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30353-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-30353-1_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30352-4
Online ISBN: 978-3-642-30353-1
eBook Packages: Computer ScienceComputer Science (R0)