{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,7]],"date-time":"2025-07-07T11:05:06Z","timestamp":1751886306592,"version":"3.37.0"},"reference-count":71,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2009,5,26]],"date-time":"2009-05-26T00:00:00Z","timestamp":1243296000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Program."],"published-print":{"date-parts":[[2011,4]]},"DOI":"10.1007\/s10107-009-0285-6","type":"journal-article","created":{"date-parts":[[2009,5,25]],"date-time":"2009-05-25T14:17:29Z","timestamp":1243261049000},"page":"297-343","source":"Crossref","is-referenced-by-count":2,"title":["Efficient branch-and-bound algorithms for weighted MAX-2-SAT"],"prefix":"10.1007","volume":"127","author":[{"given":"Toshihide","family":"Ibaraki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Takashi","family":"Imamichi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuichi","family":"Koga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hiroshi","family":"Nagamochi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Koji","family":"Nonobe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mutsunori","family":"Yagiura","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,5,26]]},"reference":[{"unstructured":"Alsinet, T., Manya, F., Planes, J.: Improved branch and bound algorithms for Max-SAT. In: Sixth International Conference on Theory and Applications of Satisfiability Testing, pp. 408\u2013415 (2003)","key":"285_CR1"},{"key":"285_CR2","first-page":"334","volume-title":"Advances in Artificial Intelligence\u2014IBERAMIA 2004. Lecture Notes in Artificial Intelligence, vol. 3315","author":"T. Alsinet","year":"2004","unstructured":"Alsinet T., Many\u00e0 F., Planes J.: A Max-SAT solver with lazy data structures. In: Lema\u00eetre, C., Reyes, C.A., Gonzalez, J.A. (eds) Advances in Artificial Intelligence\u2014IBERAMIA 2004. Lecture Notes in Artificial Intelligence, vol. 3315, pp. 334\u2013342. Springer, Heidelberg (2004)"},{"key":"285_CR3","first-page":"317","volume-title":"New Ideas in Optimization","author":"M.M. Amini","year":"1999","unstructured":"Amini M.M., Alidaee B., Kochenberger G.A.: A scatter search approach to unconstrained quadratic binary programs. In: Corne, D., Dorigo, M., Glover, F. (eds) New Ideas in Optimization, pp. 317\u2013329. McGraw-Hill, London (1999)"},{"key":"285_CR4","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B. Aspvall","year":"1979","unstructured":"Aspvall B., Plass M.R., Tarjan R.E.: A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Inf. Process. Lett. 8, 121\u2013123 (1979)","journal-title":"Inf. Process. Lett."},{"doi-asserted-by":"crossref","unstructured":"Bansal, N., Raman, V.: Upper bounds for MaxSat: Further improved. In: ISAAC \u201999: Proceedings of the 10th International Symposium on Algorithms and Computation, pp. 247\u2013258. Springer-Verlag, London (1999)","key":"285_CR5","DOI":"10.1007\/3-540-46632-0_26"},{"key":"285_CR6","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1016\/j.orl.2005.07.001","volume":"34","author":"P. Bonami","year":"2006","unstructured":"Bonami P., Minoux M.: Exact MAX-2SAT solution via lift-and-project closure. Oper. Res. Lett. 34, 387\u2013393 (2006)","journal-title":"Oper. Res. Lett."},{"key":"285_CR7","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1023\/A:1009725216438","volume":"2","author":"B. Borchers","year":"1999","unstructured":"Borchers B., Furman J.: A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems. J. Combin. Optim. 2, 299\u2013306 (1999)","journal-title":"J. Combin. Optim."},{"unstructured":"Boros, E.: Private communication via e-mail exchange (2007)","key":"285_CR8"},{"unstructured":"Boros, E., Hammer, P.L.: A max-flow approach to improved roof-duality in quadratic 0\u20131 minimization. RUTCOR Research Report RRR 15-1989, RUTCOR (1989)","key":"285_CR9"},{"key":"285_CR10","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/S0166-218X(01)00341-9","volume":"123","author":"E. Boros","year":"2002","unstructured":"Boros E., Hammer P.L.: Pseudo-Boolean optimization. Discrete Appl. Math. 123, 155\u2013225 (2002)","journal-title":"Discrete Appl. Math."},{"key":"285_CR11","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0167-6377(90)90044-6","volume":"9","author":"E. Boros","year":"1990","unstructured":"Boros E., Crama Y., Hammer P.L.: Upper-bounds for quadratic 0\u20131 maximization. Oper. Res. Lett. 9, 73\u201379 (1990)","journal-title":"Oper. Res. Lett."},{"key":"285_CR12","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1137\/0405014","volume":"5","author":"E. Boros","year":"1992","unstructured":"Boros E., Crama Y., Hammer P.L.: Chv\u00e1tal cuts and odd cycle inequalities in quadratic 0\u20131 optimization. SIAM J. Discrete Math. 5, 163\u2013177 (1992)","journal-title":"SIAM J. Discrete Math."},{"unstructured":"Boros, E., Hammer, P.L., Tavares, G.: Preprocessing of unconstrained quadratic binary optimization. RUTCOR Research Report RRR 10-2006, RUTCOR (2006)","key":"285_CR13"},{"key":"285_CR14","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1016\/j.disopt.2007.02.001","volume":"5","author":"E. Boros","year":"2008","unstructured":"Boros E., Hammer P.L., Sun R., Tavares G.: A max-flow approach to improved lower bounds for quadratic unconstrained binary optimization (QUBO). Discrete Optim. 5, 501\u2013529 (2008)","journal-title":"Discrete Optim."},{"unstructured":"Bourjolly, J.-M., Hammer, P.L., Pulleyblank, W.R., Simeone, B.: Combinatorial methods for bounding quadratic pseudo-Boolean functions. RUTCOR Research Report RRR 27-1989, RUTCOR (1989)","key":"285_CR15"},{"key":"285_CR16","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/B978-0-08-040806-4.50007-1","volume-title":"Computer Science and Operations Research: New Developments in their Interfaces","author":"J.-M. Bourjolly","year":"1992","unstructured":"Bourjolly J.-M., Hammer P.L., Pulleyblank W.R., Simeone B.: Boolean-combinatorial bounding of maximum 2-satisfiability. In: Balci, O., Sharda, R., Zenios, S.A. (eds) Computer Science and Operations Research: New Developments in their Interfaces, pp. 23\u201342. Pergamon Press, Oxford (1992)"},{"key":"285_CR17","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/PL00009180","volume":"19","author":"B.V. Cherkassky","year":"1997","unstructured":"Cherkassky B.V., Goldberg A.V.: On implementing the push-relabel method for the maximum flow problem. Algorithmica 19, 390\u2013410 (1997)","journal-title":"Algorithmica"},{"key":"285_CR18","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"2001","unstructured":"Cormen T.H., Leiserson C.E., Rivest R.L., Stein C.: Introduction to Algorithms. MIT Press, Cambridge (2001)"},{"key":"285_CR19","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis M., Putnam H.: A computing procedure for quantification theory. J. ACM 7, 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"285_CR20","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/978-3-540-45193-8_25","volume-title":"Principles and Practice of Constraint Programming (CP 2003). Lecture Notes in Computer Science, vol. 2833","author":"S. Givry de","year":"2003","unstructured":"de Givry S., Larrosa J., Meseguer P., Schiex T.: Solving Max-SAT as weighted CSP. In: Rossi, F. (eds) Principles and Practice of Constraint Programming (CP 2003). Lecture Notes in Computer Science, vol. 2833, pp. 363\u2013376. Springer, Heidelberg (2003)"},{"key":"285_CR21","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1142\/9789812778215_0012","volume-title":"Combinatorial and Global Optimization. Series on Applied Optimization, vol. 14","author":"E. Klerk de","year":"2002","unstructured":"de Klerk E., Warners J.P.: Semidefinite programming approaches for MAX-2-SAT and MAX-3-SAT: Computational perspectives. In: Pardalos, P.M., Migdalas, A., Burkard, R.E. (eds) Combinatorial and Global Optimization. Series on Applied Optimization, vol. 14, pp. 161\u2013176. World Scientific Publishers, Singapore (2002)"},{"key":"285_CR22","first-page":"502","volume-title":"Theory and Applications of Satisfiability Testing\u2014SAT 2003. Lecture Notes in Computer Science, vol. 2919","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n N., S\u00f6rensson N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds) Theory and Applications of Satisfiability Testing\u2014SAT 2003. Lecture Notes in Computer Science, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"285_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/SAT190014","volume":"2","author":"N. E\u00e9n","year":"2006","unstructured":"E\u00e9n N., S\u00f6rensson N.: Translating pseudo-Boolean constraints into SAT. J. Satisfiability Boolean Model. Comput. 2, 1\u201325 (2006)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"285_CR24","doi-asserted-by":"crossref","first-page":"691","DOI":"10.1137\/0205048","volume":"5","author":"S. Even","year":"1976","unstructured":"Even S., Itai A., Shamir A.: On the complexity of timetable and multicommodity flow problems. SIAM J. Comput. 5, 691\u2013703 (1976)","journal-title":"SIAM J. Comput."},{"key":"285_CR25","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0304-3975(76)90059-1","volume":"1","author":"M.R. Garey","year":"1976","unstructured":"Garey M.R., Johnson D.S., Stockmeyer L.: Some simplified NP-complete graph problems. Theor. Comput. Sci. 1, 237\u2013267 (1976)","journal-title":"Theor. Comput. Sci."},{"key":"285_CR26","doi-asserted-by":"crossref","first-page":"849","DOI":"10.1287\/opre.9.6.849","volume":"9","author":"P.C. Gilmore","year":"1961","unstructured":"Gilmore P.C., Gomory R.E.: A linear programming approach to the cutting stock problem. Oper. Res. 9, 849\u2013859 (1961)","journal-title":"Oper. Res."},{"key":"285_CR27","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1287\/mnsc.44.3.336","volume":"44","author":"F. Glover","year":"1998","unstructured":"Glover F., Kochenberger G., Alidaee B.: Adaptive memory tabu search for binary quadratic programs. Manage. Sci. 44, 336\u2013345 (1998)","journal-title":"Manage. Sci."},{"key":"285_CR28","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-1-4615-5775-3_7","volume-title":"Meta-Heuristics: Advances and Trends in Local Search Paradigms for Optimization","author":"F. Glover","year":"1999","unstructured":"Glover F., Kochenberger G., Alidaee B., Amini M.: Tabu search with critical event memory: An enhanced application for binary quadratic programs. In: Voss, S., Martello, S., Osman, I.H., Roucairol, C. (eds) Meta-Heuristics: Advances and Trends in Local Search Paradigms for Optimization, pp. 93\u2013109. Kluwer Academic Publishers, Boston (1999)"},{"key":"285_CR29","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1016\/S0377-2217(01)00209-0","volume":"137","author":"F. Glover","year":"2002","unstructured":"Glover F., Alidaee B., Rego C., Kochenberger G.: One-pass heuristics for large-scale unconstrained binary quadratic problems. Eur. J. Oper. Res. 137, 272\u2013287 (2002)","journal-title":"Eur. J. Oper. Res."},{"key":"285_CR30","doi-asserted-by":"crossref","first-page":"921","DOI":"10.1145\/48014.61051","volume":"35","author":"A.V. Goldberg","year":"1988","unstructured":"Goldberg A.V., Tarjan R.E.: A new approach to the maximum-flow problem. J. ACM 35, 921\u2013940 (1988)","journal-title":"J. ACM"},{"doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT solver. In: Design Automation and Test in Europe (DATE 2002), pp. 142\u2013149 (2002)","key":"285_CR31","DOI":"10.1109\/DATE.2002.998262"},{"doi-asserted-by":"crossref","unstructured":"Gramm, J., Niedermeier, R.: Faster exact solutions for MAX2SAT. In: Conference on Algorithms and Complexity, pp. 174\u2013186 (2000)","key":"285_CR32","DOI":"10.1007\/3-540-46521-9_15"},{"key":"285_CR33","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF02612354","volume":"28","author":"P.L. Hammer","year":"1984","unstructured":"Hammer P.L., Hansen P., Simeone B.: Roof duality, complementation and persistency in quadratic 0\u20131 optimization. Math. Program. 28, 121\u2013155 (1984)","journal-title":"Math. Program."},{"key":"285_CR34","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/BF02241270","volume":"44","author":"P. Hansen","year":"1990","unstructured":"Hansen P., Jaumard B.: Algorithms for the maximum satisfiability problem. Computing 44, 279\u2013303 (1990)","journal-title":"Computing"},{"key":"285_CR35","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-3-540-72788-0_8","volume-title":"Theory and Applications of Satisfiability Testing\u2014SAT 2007. Lecture Notes in Computer Science, vol. 4501","author":"F. Heras","year":"2007","unstructured":"Heras F., Larrosa J., Oliveras A.: MiniMaxSAT: a new weighted Max-SAT solver. In: Marques-Silva, J., Sakallah, K.A. (eds) Theory and Applications of Satisfiability Testing\u2014SAT 2007. Lecture Notes in Computer Science, vol. 4501, pp. 41\u201355. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"Hirsch, E.A.: A new algorithm for MAX-2-SAT. In: STACS 2000: 17th Annual Symposium on Theoretical Aspects of Computer Science, pp. 65\u201373 (2000)","key":"285_CR36","DOI":"10.1007\/3-540-46541-3_5"},{"key":"285_CR37","first-page":"446","volume-title":"Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 443","author":"D.S. Johnson","year":"1990","unstructured":"Johnson D.S.: Local optimization and the traveling salesman problem. In: Paterson, M.S. (eds) Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 443, pp. 446\u2013461. Springer, Heidelberg (1990)"},{"unstructured":"Joy, S., Mitchell, J.E., Borchers, B.: Solving MAX-SAT and weighted MAX-SAT problems using branch-and-cut. Technical report, Mathematical Sciences, Rensselaer Polytechnic Institute, Troy, NY 12180 (1998)","key":"285_CR38"},{"key":"285_CR39","doi-asserted-by":"crossref","first-page":"1297","DOI":"10.1126\/science.264.5163.1297","volume":"264","author":"S. Kirkpatrick","year":"1994","unstructured":"Kirkpatrick S., Selman B.: Critical behavior in the satisfiability of random Boolean expressions. Science 264, 1297\u20131301 (1994)","journal-title":"Science"},{"key":"285_CR40","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1504\/IJOR.2005.007435","volume":"1","author":"G. Kochenberger","year":"2005","unstructured":"Kochenberger G., Glover F., Alidaee B., Lewis K.: Using the unconstrained quadratic program to model and solve Max 2-SAT problems. Int. J. Oper. Res. 1, 89\u2013100 (2005)","journal-title":"Int. J. Oper. Res."},{"doi-asserted-by":"crossref","unstructured":"Koga, Y.: Efficient branch-and-bound algorithms for weighted MAX-2-SAT. Master\u2019s thesis, Department of Applied Mathematics and Physics, Graduate School of Informatics, Kyoto University (2006)","key":"285_CR41","DOI":"10.1142\/9781860948534_0018"},{"key":"285_CR42","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1613\/jair.2215","volume":"30","author":"C.-M. Li","year":"2007","unstructured":"Li C.-M., Manya F., Planes J.: New inference rules for Max-SAT. J. Artif. Intell. Res. 30, 321\u2013359 (2007)","journal-title":"J. Artif. Intell. Res."},{"key":"285_CR43","first-page":"321","volume-title":"Handbook of Metaheuristics","author":"H.R. Louren\u00e7o","year":"2003","unstructured":"Louren\u00e7o H.R., Martin O.C., St\u00fctzle T.: Iterated local search. In: Glover, F., Kochenberger, G.A. (eds) Handbook of Metaheuristics, pp. 321\u2013353. Kluwer Academic Publishers, Boston (2003)"},{"key":"285_CR44","doi-asserted-by":"crossref","first-page":"551","DOI":"10.1007\/BF01553908","volume":"4","author":"M. Luby","year":"1989","unstructured":"Luby M., Ragde P.: A bidirectional shortest-path algorithm with good average-case behavior. Algorithmica 4, 551\u2013567 (1989)","journal-title":"Algorithmica"},{"key":"285_CR45","first-page":"360","volume-title":"Theory and Applications of Satisfiability Testing\u2014SAT 2004. Lecture Notes in Computer Science, vol. 3542","author":"Y.S. Mahajan","year":"2005","unstructured":"Mahajan Y.S., Fu Z., Malik S.: Zchaff2004: An efficient SAT solver. In: Hoos, H.H., Mitchell, D.G. (eds) Theory and Applications of Satisfiability Testing\u2014SAT 2004. Lecture Notes in Computer Science, vol. 3542, pp. 360\u2013375. Springer, Heidelberg (2005)"},{"key":"285_CR46","first-page":"299","volume":"5","author":"O. Martin","year":"1991","unstructured":"Martin O., Otto S.W., Felten E.W.: Large-step Markov chains for the traveling salesman problem. Complex Syst. 5, 299\u2013326 (1991)","journal-title":"Complex Syst."},{"key":"285_CR47","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1023\/A:1017912624016","volume":"8","author":"P. Merz","year":"2002","unstructured":"Merz P., Freisleben B.: Greedy and local search heuristics for unconstrained binary quadratic programming. J. Heuristics 8, 197\u2013213 (2002)","journal-title":"J. Heuristics"},{"key":"285_CR48","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/j.orl.2004.06.004","volume":"33","author":"R. Miyashiro","year":"2005","unstructured":"Miyashiro R., Matsui T.: A polynomial-time algorithm to find an equitable home-away assignment. Oper. Res. Lett. 33, 235\u2013241 (2005)","journal-title":"Oper. Res. Lett."},{"key":"285_CR49","doi-asserted-by":"crossref","first-page":"1975","DOI":"10.1016\/j.cor.2004.09.030","volume":"33","author":"R. Miyashiro","year":"2006","unstructured":"Miyashiro R., Matsui T.: Semidefinite programming based approaches to the break minimization problem. Comput. Oper. Res. 33, 1975\u20131982 (2006)","journal-title":"Comput. Oper. Res."},{"doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 39th Design Automation Conference (DAC 2001), pp. 530\u2013535 (2001)","key":"285_CR50","DOI":"10.1145\/378239.379017"},{"key":"285_CR51","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1006\/jagm.2000.1075","volume":"36","author":"R. Niedermeier","year":"2000","unstructured":"Niedermeier R., Rossmanith P.: New upper bounds for maximum satisfiability. J. Algorithms 36, 63\u201388 (2000)","journal-title":"J. Algorithms"},{"key":"285_CR52","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1090\/dimacs\/035\/11","volume":"35","author":"M.G.C. Resende","year":"1997","unstructured":"Resende M.G.C., Pitsoulis L.S., Pardalos P.M.: Approximate solution of weighted MAX-SAT problems using GRASP. DIMACS Ser. Discrete Math. Theor. Comput. Sci. 35, 393\u2013405 (1997)","journal-title":"DIMACS Ser. Discrete Math. Theor. Comput. Sci."},{"unstructured":"Selman, B., Levesque, H.J., Mitchell, D.: A new method for solving hard satisfiability problems. In: Rosenbloom, P., Szolovits, P. (eds.) Proceedings of the Tenth National Conference on Artificial Intelligence, pp. 440\u2013446. AAAI Press, Menlo Park (1992)","key":"285_CR53"},{"unstructured":"Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI\u201994), pp. 337\u2013343. Seattle (1994)","key":"285_CR54"},{"doi-asserted-by":"crossref","unstructured":"Shen, H., Zhang, H.: An empirical study of MAX-2-SAT phase transitions. In: LICS\u201903 Workshop on Typical Case Complexity and Phase Transitions, June (2003)","key":"285_CR55","DOI":"10.1016\/S1571-0653(04)00464-0"},{"doi-asserted-by":"crossref","unstructured":"Shen, H., Zhang, H.: Improving exact algorithms for MAX-2-SAT. In: Eighth International Symposium on Artificial Intelligence and Mathematics, January (2004)","key":"285_CR56","DOI":"10.1007\/s10472-005-7036-z"},{"unstructured":"Shen, H., Zhang, H.: Study of lower bound functions for MAX-2-SAT. In: 19th National Conference on Artificial Intelligence (AAAI), pp. 185\u2013190 (2004)","key":"285_CR57"},{"unstructured":"Simeone, B.: A generalized consensus approach to nonlinear 0\u20131 minimization. Technical Report CORR 38\/79, Department of Combinatorics and Optimization, University of Waterloo (1979)","key":"285_CR58"},{"unstructured":"Simeone, B.: Quadratic 0\u20131 Programming, Boolean Functions, and Graphs. Ph.D. dissertation, Department of Combinatorics and Optimization, University of Waterloo (1979)","key":"285_CR59"},{"doi-asserted-by":"crossref","unstructured":"Smyth K., Hoos H.H., St\u00fctzle T.: Iterated robust tabu search for MAX-SAT. In: Xiang, Y., Brahim, C.-D. Advances in Artificial Intelligence: 16th Conference of the Canadian Society for Computational Studies of Intelligence (AI 2003). Lecture Notes in Artificial Intelligence, vol. 2671, pp. 129\u2013144. Springer, Heidelberg (2003)","key":"285_CR60","DOI":"10.1007\/3-540-44886-1_12"},{"unstructured":"Tavares, G.: Max2SatGen: A generator of weighted MAX-2-SAT formulas. RUTCOR, Rutgers University (2005)","key":"285_CR61"},{"key":"285_CR62","first-page":"306","volume-title":"Theory and Applications of Satisfiability Testing\u2014SAT 2004. Lecture Notes in Computer Science, vol. 3542","author":"D.A.D. Tompkins","year":"2005","unstructured":"Tompkins D.A.D., Hoos H.H.: UBCSAT: An implementation and experimentation environment for SLS algorithms for SAT and MAX-SAT. In: Hoos, H.H., Mitchell, D.G. (eds) Theory and Applications of Satisfiability Testing\u2014SAT 2004. Lecture Notes in Computer Science, vol. 3542, pp. 306\u2013320. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Trick, M.A.: A schedule-then-break approach to sports timetabling. In: PATAT \u201900: Selected papers from the Third International Conference on Practice and Theory of Automated Timetabling III, pp. 242\u2013253. Springer, Heidelberg (2001)","key":"285_CR63","DOI":"10.1007\/3-540-44629-X_15"},{"doi-asserted-by":"crossref","unstructured":"Wallace, R.J.: Enhancing maximum satisfiability algorithms with pure literal strategies. In: McCalla, G. (ed.) Advances in Artificial Intelligence: 11th Biennial Conference of the Canadian Society for Computational Studies of Intelligence (AI96). Lecture Notes in Computer Science, vol. 1081 (1996)","key":"285_CR64","DOI":"10.1007\/3-540-61291-2_67"},{"doi-asserted-by":"crossref","unstructured":"Wallace, R.J., Freuder, E.C.: Comparative studies of constraint satisfaction and Davis-Putnam algorithms for maximum satisfiability problems. In: Johnson, D.S., Trick, M.A. (eds.) Cliques, Coloring, and Satisfiability. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, pp. 587\u2013615 (1996)","key":"285_CR65","DOI":"10.1090\/dimacs\/026\/28"},{"key":"285_CR66","doi-asserted-by":"crossref","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. 164, 47\u201380 (2005)","journal-title":"Artif. Intell."},{"key":"285_CR67","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1023\/A:1009873324187","volume":"3","author":"M. Yagiura","year":"1999","unstructured":"Yagiura M., Ibaraki T.: Analyses on the 2 and 3-flip neighborhoods for the MAX SAT. J. Combin. Optim. 3, 95\u2013114 (1999)","journal-title":"J. Combin. Optim."},{"key":"285_CR68","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1023\/A:1011306011437","volume":"7","author":"M. Yagiura","year":"2001","unstructured":"Yagiura M., Ibaraki T.: Efficient 2 and 3-flip neighborhood search algorithms for the MAX SAT: Experimental evaluation. J. Heuristics 7, 423\u2013442 (2001)","journal-title":"J. Heuristics"},{"key":"285_CR69","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1006\/jagm.1994.1045","volume":"17","author":"M. Yannakakis","year":"1994","unstructured":"Yannakakis M.: On the approximation of maximum satisfiability. J. Algorithms 17, 475\u2013502 (1994)","journal-title":"J. Algorithms"},{"doi-asserted-by":"crossref","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: Proceedings of the International Conference on Automated Deduction (CADE\u201997), pp. 272\u2013275 (1997)","key":"285_CR70","DOI":"10.1007\/3-540-63104-6_28"},{"issue":"1","key":"285_CR71","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1016\/S1571-0661(04)80663-7","volume":"86","author":"H. Zhang","year":"2003","unstructured":"Zhang H., Shen H., Many\u00e0 F.: Exact algorithms for MAX-SAT. Electronic Notes in Theoretical Computer Science 86(1), 190\u2013203 (2003)","journal-title":"Electronic Notes in Theoretical Computer Science"}],"container-title":["Mathematical Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10107-009-0285-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10107-009-0285-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10107-009-0285-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,9]],"date-time":"2025-02-09T17:59:35Z","timestamp":1739123975000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10107-009-0285-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,5,26]]},"references-count":71,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,4]]}},"alternative-id":["285"],"URL":"https:\/\/doi.org\/10.1007\/s10107-009-0285-6","relation":{},"ISSN":["0025-5610","1436-4646"],"issn-type":[{"type":"print","value":"0025-5610"},{"type":"electronic","value":"1436-4646"}],"subject":[],"published":{"date-parts":[[2009,5,26]]}}}