{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T14:40:01Z","timestamp":1748788801989,"version":"3.41.0"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2016,2,25]],"date-time":"2016-02-25T00:00:00Z","timestamp":1456358400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100006280","name":"Ministerio de Ciencia y Tecnolog\u00eda (ES)","doi-asserted-by":"publisher","award":["TIN2013-48031-C4-4-P","TIN2014-53234-C2-2-R"],"award-info":[{"award-number":["TIN2013-48031-C4-4-P","TIN2014-53234-C2-2-R"]}],"id":[{"id":"10.13039\/501100006280","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2016,6]]},"DOI":"10.1007\/s10472-016-9502-1","type":"journal-article","created":{"date-parts":[[2016,2,25]],"date-time":"2016-02-25T14:15:12Z","timestamp":1456409712000},"page":"43-66","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On the performance of MaxSAT and MinSAT solvers on 2SAT-MaxOnes"],"prefix":"10.1007","volume":"77","author":[{"given":"Josep","family":"Argelich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ram\u00f3n","family":"B\u00e9jar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e8sar","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carles","family":"Mateu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1861-9736","authenticated-orcid":false,"given":"Jordi","family":"Planes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,2,25]]},"reference":[{"key":"9502_CR1","unstructured":"Abram\u00e9, A., Habet, D.: On the resiliency of unit propagation to max-resolution. In: proceedings of the 24th International Joint Conference on Artificial Intelligence (2015)"},{"key":"9502_CR2","doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial maxSAT through satisfiability testing. In: Proceedings of SAT, vol. 2009, pp 427\u2013440 (2009)","DOI":"10.1007\/978-3-642-02777-2_39"},{"key":"9502_CR3","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/j.artint.2013.01.002","volume":"196","author":"C Ans\u00f3tegui","year":"2013","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: Sat-based maxsat algorithms. Artif. Intell. 196, 77\u2013105 (2013)","journal-title":"Artif. Intell."},{"key":"9502_CR4","doi-asserted-by":"crossref","unstructured":"Argelich, J., B\u00e9jar, R., Fern\u00e1ndez, C., Mateu, C.: On 2sat-maxones with unbalanced polarity: from easy problems to hard maxclique problems. In: proceedings of CCIA\u20192011, volume 232 of Frontiers in Artificial Intelligence and Applications, pp 21\u201330. IOS Press (2011)","DOI":"10.3233\/978-1-60750-842-7-21"},{"issue":"2\u20134","key":"9502_CR5","first-page":"251","volume":"4","author":"J Argelich","year":"2008","unstructured":"Argelich, J., Li, C.M., Many\u00e0, F., Planes, J.: The first and second maxSAT evaluations. JSAT 4(2\u20134), 251\u2013278 (2008)","journal-title":"JSAT"},{"key":"9502_CR6","unstructured":"Argelich, J., Lynce, I., Marques-Silva, J.P.: On solving boolean multilevel optimization problems. In: Proceedings of IJCAI, vol. 2009, pp 393\u2013398 (2009)"},{"key":"9502_CR7","unstructured":"Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.). IOS Press (2009)"},{"key":"9502_CR8","unstructured":"Bjorner, N., Narodytska, N.: Maximum satisfiability using cores and correction sets. In: proceedings of the 24th International Joint Conference on Artificial Intelligence (2015)"},{"key":"9502_CR9","unstructured":"Cha, B., Iwama, K., Kambayashi, Y., Miyazaki, S.: Local search algorithms for partial maxSAT. In: AAAI\u201997, pp 263\u2013268 (1997)"},{"key":"9502_CR10","doi-asserted-by":"crossref","unstructured":"Chen, Y., Safarpour, S., Veneris, A.G., Marques-Silva, J.P.: Spatial and temporal design debug using partial maxSAT. In: Proceedings of 19th ACM Great Lakes Symposium on VLSI, pp 345\u2013350 (2009)","DOI":"10.1145\/1531542.1531621"},{"key":"9502_CR11","doi-asserted-by":"crossref","unstructured":"Conrad, J., Gomes, C.P., van Hoeve, W.J., Sabharwal, A., Suter, J.: Connections in networks Hardness of feasibility versus optiMality. In: Proceedings of CPAIOR2007, pp 16\u201328 (2007)","DOI":"10.1007\/978-3-540-72397-4_2"},{"issue":"3","key":"9502_CR12","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1006\/jcss.1996.0081","volume":"53","author":"A Goerdt","year":"2006","unstructured":"Goerdt, A.: A threshold for unsatisfiability. J. Comput. Syst. Sci. 53(3), 469\u2013486 (2006)","journal-title":"J. Comput. Syst. Sci."},{"key":"9502_CR13","unstructured":"Gra\u00e7a, A., Lynce, I., Marques-Silva, J., Oliveira, A.L.: Haplotype inference combining pedigrees and unrelated individuals. In: WCB09, pp 27\u201336 (2009)"},{"key":"9502_CR14","doi-asserted-by":"crossref","unstructured":"H\u00e5stad, J.: Clique is hard to approximate within n (1\u2212\ud835\udf16). In: FOCS\u201906, pp 627\u2013636 (1996)","DOI":"10.1109\/SFCS.1996.548522"},{"key":"9502_CR15","unstructured":"Li, C.M., Many\u00e0, F.: An exact inference scheme for minsat. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence (2015)"},{"issue":"4","key":"9502_CR16","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/s10601-010-9097-9","volume":"15","author":"CM Li","year":"2010","unstructured":"Li, C.M., Many\u00e0, F., Mohamedou, N.O., Planes, J.: Resolution-based lower bounds in maxSAT. Constraints 15(4), 456\u2013484 (2010)","journal-title":"Constraints"},{"key":"9502_CR17","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1613\/jair.2215","volume":"30","author":"CM Li","year":"2007","unstructured":"Li, C.M., Many\u00e0, F., Planes, J.: New inference rules for Max-SAT. J. Artif Intell. Res. (JAIR) 30, 321\u2013359 (2007)","journal-title":"J. Artif Intell. Res. (JAIR)"},{"key":"9502_CR18","doi-asserted-by":"crossref","unstructured":"Li, C.M., Quan, Z.: An efficient branch-and-bound algorithm based on maxSAT for the maximum clique problem. In: proceedings of AAAI\u201910, pp 128\u2013133 (2010)","DOI":"10.1609\/aaai.v24i1.7536"},{"key":"9502_CR19","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1016\/j.artint.2012.05.004","volume":"190","author":"CM Li","year":"2012","unstructured":"Li, C.M., Zhu, Z., Many\u00e0, F., Simon, L.: Optimizing with minimum satisfiability. Artif. Intell. 190, 32\u201344 (2012)","journal-title":"Artif. Intell."},{"issue":"3-4","key":"9502_CR20","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/s10472-011-9233-2","volume":"62","author":"J Marques-Silva","year":"2011","unstructured":"Marques-Silva, J., Argelich, J., Gra\u00e7a, A., Lynce, I.: Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell. 62(3-4), 317\u2013343 (2011)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9502_CR21","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V.M., Lynce, I.: Open-WBO A modular maxsat solver. In: Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, pp 438\u2013445. Proceedings, Vienna, Austria (2014)","DOI":"10.1007\/978-3-319-09284-3_33"},{"key":"9502_CR22","doi-asserted-by":"crossref","unstructured":"Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided maxsat with soft cardinality constraints. In: Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, pp 564\u2013573. Proceedings, Lyon, France (2014)","DOI":"10.1007\/978-3-319-10428-7_41"},{"issue":"4","key":"9502_CR23","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/s10601-013-9146-2","volume":"18","author":"A Morgado","year":"2013","unstructured":"Morgado, A., Heras, F., Liffiton, M.H., 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":"9502_CR24","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/s10601-010-9095-y","volume":"15","author":"ED Rosa","year":"2010","unstructured":"Rosa, E.D., Giunchiglia, E., Maratea, M.: Solving satisfiability problems with preferences. Constraints 15, 485\u2013515 (2010)","journal-title":"Constraints"},{"key":"9502_CR25","unstructured":"Slaney, J.K., Walsh, T.: Phase transition behavior: from decision to optimization. In: Proceedings of SAT2002 (2002)"},{"key":"9502_CR26","doi-asserted-by":"crossref","unstructured":"Zhang, W.: Phase transitions and backbones of 3-SAT and maximum 3-SAT. In: Proceedings of CP 2001, pp 153\u2013167. Springer (2001)","DOI":"10.1007\/3-540-45578-7_11"},{"issue":"1-2","key":"9502_CR27","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0004-3702(95)00054-2","volume":"81","author":"W Zhang","year":"1996","unstructured":"Zhang, W., Korf, R.E.: A study of complexity transitions on the asymmetric traveling salesman problem. Artif. Intell. 81(1-2), 223\u2013239 (1996)","journal-title":"Artif. Intell."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-016-9502-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-016-9502-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-016-9502-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T14:25:56Z","timestamp":1748787956000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-016-9502-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,2,25]]},"references-count":27,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["9502"],"URL":"https:\/\/doi.org\/10.1007\/s10472-016-9502-1","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2016,2,25]]}}}