{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:08:53Z","timestamp":1748664533323,"version":"3.41.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243177"},{"type":"electronic","value":"9783319243184"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24318-4_20","type":"book-chapter","created":{"date-parts":[[2015,9,11]],"date-time":"2015-09-11T05:42:56Z","timestamp":1441950176000},"page":"272-286","source":"Crossref","is-referenced-by-count":8,"title":["Exploiting Resolution-Based Representations for MaxSAT Solving"],"prefix":"10.1007","author":[{"given":"Miguel","family":"Neves","sequence":"first","affiliation":[]},{"given":"Ruben","family":"Martins","sequence":"additional","affiliation":[]},{"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"additional","affiliation":[]},{"given":"In\u00eas","family":"Lynce","sequence":"additional","affiliation":[]},{"given":"Vasco","family":"Manquinho","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,27]]},"reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-642-31612-8_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"C Ans\u00f3tegui","year":"2012","unstructured":"Ans\u00f3tegui, C., Gir\u00e1ldez-Cru, J., Levy, J.: The Community structure of SAT formulas. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 410\u2013423. Springer, Heidelberg (2012)"},{"issue":"1","key":"20_CR2","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/s10479-012-1081-x","volume":"218","author":"R As\u00edn","year":"2014","unstructured":"As\u00edn, R., Nieuwenhuis, R.: Curriculum-based course timetabling with SAT and MaxSAT. Annals of Operations Research 218(1), 71\u201391 (2014)","journal-title":"Annals of Operations Research"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"O Bailleux","year":"2003","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108\u2013122. Springer, Heidelberg (2003)"},{"issue":"10","key":"20_CR4","doi-asserted-by":"publisher","first-page":"P10008","DOI":"10.1088\/1742-5468\/2008\/10\/P10008","volume":"2008","author":"V Blondel","year":"2008","unstructured":"Blondel, V., Guillaume, J., Lambiotte, R., Lefebvre, E.: Fast unfolding of communities in large networks. Journal of Statistical Mechanics 2008(10), P10008 (2008)","journal-title":"Journal of Statistical Mechanics"},{"key":"20_CR5","unstructured":"Brandes, U., Delling, D., Gaertler, M., Goerke, R., Hoefer, M., Nikoloski, Z., Wagner, D.: Maximizing modularity is hard (2006). arXiv: physics\/0608255"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11814948_25","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"Z Fu","year":"2006","unstructured":"Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252\u2013265. Springer, Heidelberg (2006)"},{"issue":"12","key":"20_CR7","doi-asserted-by":"publisher","first-page":"7821","DOI":"10.1073\/pnas.122653799","volume":"99","author":"M Girvan","year":"2002","unstructured":"Girvan, M., Newman, M.E.J.: Community structure in social and biological networks. Proceedings of the National Academy of Sciences 99(12), 7821\u20137826 (2002)","journal-title":"Proceedings of the National Academy of Sciences"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Heras, F., Morgado, A., Marques-Silva, J.: Core-guided binary search algorithms for maximum satisfiability. In: AAAI Conference on Artificial Intelligence. AAAI Press (2011)","DOI":"10.1609\/aaai.v25i1.7822"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Ignatiev, A., Morgado, A., Manquinho, V., Lynce, I., Marques-Silva, J.: Progression in maximum satisfiability. In: European Conference on Artificial Intelligence, pp. 453\u2013458. IOS Press (2014)","DOI":"10.3233\/978-1-61499-419-0-453"},{"issue":"1\/2","key":"20_CR10","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/SAT190090","volume":"8","author":"M Janota","year":"2012","unstructured":"Janota, M., Lynce, I., Manquinho, V., Marques-Silva, J.: PackUp: Tools for Package Upgradability Solving. Journal on Satisfiability, Boolean Modeling and Computation 8(1\/2), 89\u201394 (2012)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-12002-2_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129\u2013144. Springer, Heidelberg (2010)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Programming Language Design and Implementation, pp. 437\u2013446. ACM (2011)","DOI":"10.1145\/1993316.1993550"},{"issue":"1\/2","key":"20_CR13","doi-asserted-by":"crossref","first-page":"95","DOI":"10.3233\/SAT190091","volume":"8","author":"M Koshimura","year":"2012","unstructured":"Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: A Partial Max-SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation 8(1\/2), 95\u2013100 (2012)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"20_CR14","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics 96\u201397, 149\u2013176 (1999)","journal-title":"Discrete Applied Mathematics"},{"key":"20_CR15","unstructured":"Le Berre, D., Rapicault, P.: Dependency management for the eclipse ecosystem: an update. In: International Workshop on Logic and Search"},{"key":"20_CR16","unstructured":"Marques-Silva, J., Planes, J.: On Using Unsatisfiability for Solving Maximum Satisfiability (2007). CoRR"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"531","DOI":"10.1007\/978-3-319-10428-7_39","volume-title":"Principles and Practice of Constraint Programming","author":"R Martins","year":"2014","unstructured":"Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental cardinality constraints for MaxSAT. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 531\u2013548. Springer, Heidelberg (2014)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/978-3-319-09284-3_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"R Martins","year":"2014","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a modular MaxSAT solver $$^\\text{, }$$ . In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438\u2013445. Springer, Heidelberg (2014)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-39071-5_14","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"R Martins","year":"2013","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Community-based partitioning for MaxSAT solving. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 182\u2013191. Springer, Heidelberg (2013)"},{"issue":"4","key":"20_CR20","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/s10601-013-9146-2","volume":"18","author":"A Morgado","year":"2013","unstructured":"Morgado, A., Heras, F., Liffiton, M., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints 18(4), 478\u2013534 (2013)","journal-title":"Constraints"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-642-31612-8_22","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A Morgado","year":"2012","unstructured":"Morgado, A., Heras, F., Marques-Silva, J.: Improvements to core-guided binary search for MaxSAT. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 284\u2013297. Springer, Heidelberg (2012)"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: AAAI Conference on Artificial Intelligence, pp. 2717\u20132723. AAAI Press (2014)","DOI":"10.1609\/aaai.v28i1.9124"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Newman, M.E.J., Girvan, M.: Finding and evaluating community structure in networks. Physical Review E 69(026113) (2004)","DOI":"10.1103\/PhysRevE.69.026113"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Safarpour, S., Mangassarian, H., Veneris, A.G., Liffiton, M.H., Sakallah, K.A.: Improved design debugging using maximum satisfiability. In: Formal Methods in Computer-Aided Design, pp. 13\u201319. IEEE Computer Society (2007)","DOI":"10.1109\/FMCAD.2007.4401977"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1007\/978-3-642-23786-7_59","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"A Gelder Van","year":"2011","unstructured":"Van Gelder, A.: Variable independence and resolution paths for quantified boolean formulas. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 789\u2013803. Springer, Heidelberg (2011)"},{"issue":"4","key":"20_CR26","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/0004-3702(70)90011-1","volume":"1","author":"RA Yates","year":"1970","unstructured":"Yates, R.A., Raphael, B., Hart, T.P.: Resolution graphs. Artificial Intelligence 1(4), 257\u2013289 (1970)","journal-title":"Artificial Intelligence"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing -- SAT 2015"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24318-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T15:26:29Z","timestamp":1748618789000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24318-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243177","9783319243184"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24318-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}