乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:47:12Z","timestamp":1725857232349},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319409696"},{"type":"electronic","value":"9783319409702"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40970-2_34","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T11:14:55Z","timestamp":1465557295000},"page":"539-546","source":"Crossref","is-referenced-by-count":22,"title":["LMHS: A SAT-IP Hybrid MaxSAT Solver"],"prefix":"10.1007","author":[{"given":"Paul","family":"Saikko","sequence":"first","affiliation":[]},{"given":"Jeremias","family":"Berg","sequence":"additional","affiliation":[]},{"given":"Matti","family":"J\u00e4rvisalo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"issue":"1","key":"34_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s12532-008-0001-1","volume":"1","author":"T Achterberg","year":"2009","unstructured":"Achterberg, T.: SCIP: solving constraint integer programs. Math. Program. Comput. 1(1), 1\u201341 (2009)","journal-title":"Math. Program. Comput."},{"key":"34_CR2","unstructured":"Argelich, J., Li, C.M., Many\u00e1, F., Planes, J.: Max-SAT 2015: Tenth Max-SAT Evaluation (2015). http:\/\/www.maxsat.udl.cat\/15\/"},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/978-3-642-36742-7_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Belov","year":"2013","unstructured":"Belov, A., J\u00e4rvisalo, M., Marques-Silva, J.: Formula preprocessing in MUS extraction. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 108\u2013123. Springer, Heidelberg (2013)"},{"key":"34_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/978-3-642-45221-5_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A Belov","year":"2013","unstructured":"Belov, A., Morgado, A., Marques-Silva, J.: SAT-based preprocessing for MaxSAT. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 96\u2013111. Springer, Heidelberg (2013)"},{"key":"34_CR5","unstructured":"Berg, J., Saikko, P., J\u00e4rvisalo, M.: Improving the effectiveness of SAT-based preprocessing for MaxSAT. In: Proceedings of IJCAI, pp. 239\u2013245. AAAI Press (2015)"},{"key":"34_CR6","doi-asserted-by":"crossref","unstructured":"Berg, J., Saikko, P., J\u00e4rvisalo, M.: Re-using auxiliary variables for MaxSAT preprocessing. In: Proceedings of ICTAI, pp. 813\u2013820. IEEE (2015)","DOI":"10.1109\/ICTAI.2015.120"},{"key":"34_CR7","unstructured":"Biere, A.: Yet another local search solver and Lingeling and friends entering the SAT competition 2014. In: Proceedings of SAT Competition 2014, vol. B-2014-2, pp. 39\u201340. Department of Computer Science Series of Publications B, University of Helsinki (2014)"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/978-3-642-23786-7_19","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"J Davies","year":"2011","unstructured":"Davies, J., Bacchus, F.: Solving MAXSAT by solving a sequence of simpler SAT instances. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 225\u2013239. Springer, Heidelberg (2011)"},{"key":"34_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/978-3-642-39071-5_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"J Davies","year":"2013","unstructured":"Davies, J., Bacchus, F.: Exploiting the power of MIP solvers in MaxSAT. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 166\u2013181. Springer, Heidelberg (2013)"},{"key":"34_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/978-3-642-40627-0_21","volume-title":"Principles and Practice of Constraint Programming","author":"J Davies","year":"2013","unstructured":"Davies, J., Bacchus, F.: Postponing optimization to speed up MAXSAT solving. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 247\u2013262. Springer, Heidelberg (2013)"},{"key":"34_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"34_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"2","key":"34_CR13","doi-asserted-by":"crossref","first-page":"195","DOI":"10.3233\/AIC-140636","volume":"28","author":"F Heras","year":"2015","unstructured":"Heras, F., Morgado, A., Marques-Silva, J.: MaxSAT-based encodings for group MaxSAT. AI Commun. 28(2), 195\u2013214 (2015)","journal-title":"AI Commun."},{"key":"34_CR14","unstructured":"IBM ILOG: CPLEX optimizer 12.6.0 (2014). http:\/\/www-01.ibm.com\/software\/commerce\/optimization\/cplex-optimizer\/"},{"key":"34_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"34_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-3-642-13509-5_14","volume-title":"Combinatorial Pattern Matching","author":"RM Karp","year":"2010","unstructured":"Karp, R.M.: Implicit hitting set problems and multi-genome alignment. In: Amir, A., Parida, L. (eds.) CPM 2010. LNCS, vol. 6129, pp. 151\u2013151. Springer, Heidelberg (2010)"},{"key":"34_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/978-3-642-31612-8_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"N Manthey","year":"2012","unstructured":"Manthey, N.: Coprocessor 2.0 \u2013 a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 436\u2013441. Springer, Heidelberg (2012)"},{"issue":"2","key":"34_CR18","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1287\/opre.1120.1139","volume":"61","author":"E Moreno-Centeno","year":"2013","unstructured":"Moreno-Centeno, E., Karp, R.M.: The implicit hitting set approach to solve combinatorial optimization problems with an application to multigenome alignment. Oper. Res. 61(2), 453\u2013468 (2013)","journal-title":"Oper. Res."},{"key":"34_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/978-3-319-18008-3_24","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"P Saikko","year":"2015","unstructured":"Saikko, P., Malone, B., J\u00e4rvisalo, M.: MaxSAT-based cutting planes for learning graphical models. In: Michel, L. (ed.) CPAIOR 2015. LNCS, vol. 9075, pp. 347\u2013356. Springer, Heidelberg (2015)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,22]],"date-time":"2020-09-22T01:27:50Z","timestamp":1600738070000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}