{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:58:19Z","timestamp":1725533899981},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027765"},{"type":"electronic","value":"9783642027772"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02777-2_42","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T06:58:18Z","timestamp":1245999498000},"page":"453-466","source":"Crossref","is-referenced-by-count":4,"title":["Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates"],"prefix":"10.1007","author":[{"given":"Javier","family":"Larrosa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Nieuwenhuis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Albert","family":"Oliveras","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enric","family":"Rodr\u00edguez-Carbonell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"42_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-89439-1_2","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. As\u00edn","year":"2008","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Efficient Generation of Unsatisfiability Proofs and Cores in SAT. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS, vol.\u00a05330, pp. 16\u201330. Springer, Heidelberg (2008)"},{"key":"42_CR2","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1023\/A:1009812409930","volume":"4","author":"B. Cabon","year":"1999","unstructured":"Cabon, B., et al.: Radio Link Frequency Assignment. Constraints\u00a04, 79\u201389 (1999)","journal-title":"Constraints"},{"key":"42_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-540-72788-0_32","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"A. Cimatti","year":"2007","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 334\u2013339. Springer, Heidelberg (2007)"},{"key":"42_CR4","first-page":"641","volume-title":"Proc. of DAC 1995","author":"O. Coudert","year":"1995","unstructured":"Coudert, O., Madre, J.C.: New Ideas for Solving Covering Problems. In: Proc. of DAC 1995, pp. 641\u2013646. ACM, New York (1995)"},{"key":"42_CR5","first-page":"197","volume-title":"Proc. of DAC 1996","author":"O. Coudert","year":"1996","unstructured":"Coudert, O.: On Solving Binate Covering Problems. In: Proc. of DAC 1996, pp. 197\u2013202. ACM, New York (1996)"},{"key":"42_CR6","doi-asserted-by":"crossref","unstructured":"Fu, Z., Malik, S.: Solving the Minimum Cost Satisability Problem Using SAT Based Branch-and-Bound Search. In: Proc. of ICCAD 1996, pp. 852\u2013859 (2006)","DOI":"10.1109\/ICCAD.2006.320089"},{"issue":"4","key":"42_CR7","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1145\/502175.502186","volume":"6","author":"P.F. Flores","year":"2001","unstructured":"Flores, P.F., Neto, H.C., Marques-Silva, J.P.: An Exact Solution to the Minimum Size Test Pattern Problem. ACM Trans. Des. Autom. Electron. Syst.\u00a06(4), 629\u2013644 (2001)","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"key":"42_CR8","first-page":"283","volume-title":"Proc. of SAT 2000","author":"H.H. Hoos","year":"2000","unstructured":"Hoos, H.H., St\u00fctzle, T.: SATLIB: An Online Resource for Research on SAT. In: Proc. of SAT 2000, pp. 283\u2013292. IOS Press, Amsterdam (2000), www.satlib.org"},{"key":"42_CR9","first-page":"117","volume-title":"Proc. of DAC 1997","author":"S. Liao","year":"1997","unstructured":"Liao, S., Devadas, S.: Solving Covering Problems Using LPR-Based Lower Bounds. In: Proc. of DAC 1997, pp. 117\u2013120. ACM, New York (1997)"},{"issue":"2-3","key":"42_CR10","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1016\/j.artint.2007.05.006","volume":"172","author":"J. Larrosa","year":"2008","unstructured":"Larrosa, J., Heras, F., de Givry, S.: A Logical Approach to Efficient Max-SAT Solving. Artif. Intell.\u00a0172(2-3), 204\u2013233 (2008)","journal-title":"Artif. Intell."},{"key":"42_CR11","unstructured":"Li, X.Y.: Optimization Algorithms for the Minimum-Cost Satisfiability Problem. PhD thesis, Dept. Comp. Sc., N. Carolina State Univ. (2004)"},{"key":"42_CR12","unstructured":"Makhorin, A.: GNU Linear Programming Kit (2008), http:\/\/www.gnu.org\/software\/glpk\/glpk.html"},{"key":"42_CR13","first-page":"103","volume-title":"Proc. of ECAI 2000","author":"V.M. Manquinho","year":"2000","unstructured":"Manquinho, V.M., Marques Silva, J.P.: Search Pruning Conditions for Boolean Optimization. In: Proc. of ECAI 2000, pp. 103\u2013107. IOS Press, Amsterdam (2000)"},{"issue":"5","key":"42_CR14","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1109\/43.998623","volume":"21","author":"V.M. Manquinho","year":"2002","unstructured":"Manquinho, V.M., Marques Silva, J.P.: Search Pruning Techniques in SAT-Based Branch-and-bound Algorithms for the Binate Covering Problem. IEEE Trans. on CAD of Integ. Circ. and Syst.\u00a021(5), 505\u2013516 (2002)","journal-title":"IEEE Trans. on CAD of Integ. Circ. and Syst."},{"issue":"3-4","key":"42_CR15","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1023\/B:AMAI.0000012872.46214.11","volume":"40","author":"V.M. Manquinho","year":"2004","unstructured":"Manquinho, V.M., Marques Silva, J.P.: Satisfiability-Based Algorithms for Boolean Optimization. Ann. Math. Artif. Intell.\u00a040(3-4), 353\u2013372 (2004)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"5","key":"42_CR16","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Trans. Comput.\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"42_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814948_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A.: On SAT Modulo Theories and Optimization Problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 156\u2013169. Springer, Heidelberg (2006)"},{"issue":"6","key":"42_CR18","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). Journal of the ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"42_CR19","unstructured":"Park, J.D.: Using Weighted Max-SAT Engines to Solve MPE. In: Proc. of AAAI 2002, Edmonton, Alberta, Canada, pp. 682\u2013687 (2002)"},{"key":"42_CR20","unstructured":"Sandholm, T.: An Algorithm for Optimal Winner Determination in Combinatorial Auctions. In: IJCAI 1999, pp. 542\u2013547 (1999)"},{"key":"42_CR21","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons, Chichester (1986)"},{"key":"42_CR22","unstructured":"Werner, T.: A Linear Programming Approach to Max-Sum Problem: A review. Technical Report CTU-CMP-2005-25, Center for Machine Perception, Czech Technical University (2005)"},{"issue":"1-2","key":"42_CR23","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.artint.2005.01.004","volume":"164","author":"Z. Xing","year":"2005","unstructured":"Xing, Z., Zhang, W.: Maxsolver: An Efficient Exact Algorithm for (Weighted) Maximum Satisfiability. Artif. Intell.\u00a0164(1-2), 47\u201380 (2005)","journal-title":"Artif. Intell."},{"key":"42_CR24","first-page":"10880","volume-title":"Proc. of DATE 2003","author":"L. Zhang","year":"2003","unstructured":"Zhang, L., Malik, S.: Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications. In: Proc. of DATE 2003, pp. 10880\u201310885. IEEE Computer Society, Los Alamitos (2003)"},{"key":"42_CR25","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient Conflict Driven Learning in Boolean Satisfiability Solver. In: Proc. of ICCAD 2001, pp. 279\u2013285 (2001)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T02:58:02Z","timestamp":1558407482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}