Abstract
NP-hard combinatorial optimization problems are pivotal in science and business. There exists a variety of approaches for solving such problems, but for problems with complex constraints and objective functions, local search algorithms scale the best. Such algorithms usually assume that finding a non-optimal solution with no other requirements is easy. However, what if it is NP-hard? In such case, a SAT solver can be used for finding the initial solution, but how can one continue solving the optimization problem? We offer a generic methodology, called Local Search with SAT Oracle (LSSO), to solve such problems. LSSO facilitates implementation of advanced local search methods, such as variable neighbourhood search, hill climbing and iterated local search, while using a SAT solver as an oracle. We have successfully applied our approach to solve a critical industrial problem of cell placement and productized our solution at Intel.
Chapter PDF
Similar content being viewed by others
References
E. Aarts and J. K. Lenstra. Local Search in Combinatorial Optimization. John Wiley, USA, 1st edition, 1997.
T. Achterberg. Constraint Integer Programming. PhD thesis, 2007. Chapter 1.
C. Barrett, P. Fontaine, and C. Tinelli. The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa, 2017. Available at www.SMT-LIB.org.
A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009.
N. Eén and N. Sörensson. An extensible SAT-solver. In SAT, pages 502–518, 2003.
V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In W. Damm and H. Hermanns, editors, Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3–7, 2007, Proceedings, volume 4590 of Lecture Notes in Computer Science, pages 519–531. Springer, 2007.
M. Gendreau and J.-Y. Potvin. Handbook of Metaheuristics. Springer Publishing Company, Incorporated, 2nd edition, 2010.
S. Held, B. Korte, D. Rautenbach, and J. Vygen. Combinatorial optimization in VLSI design. In V. Chvátal, editor, Combinatorial Optimization - Methods and Applications, volume 31 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 33–96. IOS Press, 2011.
D. E. Knuth. The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability. Addison Wesley, December 2015.
R. Korf, M. Moffitt, and M. Pollack. Optimal rectangle packing. Annals OR, 179:261–295, September 2010.
B. Korte and J. Vygen. Combinatorial Optimization Theory and Algorithms. Springer, 2018.
D. Kroening and O. Strichman. Bit vectors. In Decision Procedures: An Algorithmic Point of View, pages 135–156. Springer, Berlin Heidelberg, Berlin, Heidelberg, 2016.
J. Lee. A First Course in Combinatorial Optimization. Cambridge University Press, 2005.
A. Nadel. Anytime weighted MaxSAT with improved polarity selection and bit-vector optimization. In C. W. Barrett and J. Yang, editors, 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22–25, 2019, pages 193–202. IEEE, 2019.
A. Nadel. Anytime algorithms for MaxSAT and beyond. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21–24, 2020, page 1. IEEE, 2020.
A. Nadel. On optimizing a generic function in SAT. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21–24, 2020, pages 205–213. IEEE, 2020.
A. Nadel. Polarity and variable selection heuristics for SAT-based anytime MaxSAT. J. Satisf. Boolean Model. Comput., 12(1):17–22, 2020.
A. Nadel and V. Ryvchin. Efficient SAT solving under assumptions. In Theory and Applications of Satisfiability Testing - SAT 2012–15th International Conference, Trento, Italy, June 17–20, 2012. Proceedings, pages 242–255, 2012.
A. Nadel and V. Ryvchin. Bit-vector optimization. In TACAS 2016, pages 851–867, 2016.
G. L. Nemhauser and L. A. Wolsey. Integer and Combinatorial Optimization. Wiley interscience series in discrete mathematics and optimization. Wiley, 1988.
C. H. Papadimitriou and K. Steiglitz. Combinatorial Optimization: Algorithms and Complexity. Prentice-Hall, 1982.
A. Petkovska, A. Mishchenko, M. Soeken, G. D. Micheli, R. K. Brayton, and P. Ienne. Fast generation of lexicographic satisfiable assignments: enabling canonicity in SAT-based applications. In F. Liu, editor, Proceedings of the 35th International Conference on Computer-Aided Design, ICCAD 2016, Austin, TX, USA, November 7–10, 2016, page 4. ACM, 2016.
R. Poler, J. Mula, and M. Dìaz-Madroñero. Operations Research Problems: Statements and Solutions. Springer, London, 2014.
S. Prestwich. Combining the scalability of local search with the pruning techniques of systematic search. Annals of Operations Research, 115:51–72, September 2002.
F. Rothlauf. Design of Modern Heuristics. Natural Computing Series. Springer, 2011.
O. Roussel and V. M. Manquinho. Pseudo-boolean and cardinality constraints. In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 695–733. IOS Press, 2009.
R. Sebastiani and S. Tomasi. Optimization in SMT with LA(Q) cost functions. In B. Gramlich, D. Miller, and U. Sattler, editors, Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26–29, 2012. Proceedings, volume 7364 of Lecture Notes in Computer Science, pages 484–498. Springer, 2012.
N. A. Sherwani. Algorithms for VLSI physical design automation. Kluwer, 3 edition, November 1998.
E.-G. Talbi. Metaheuristics: From Design to Implementation. Wiley Publishing, 2009.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Cohen, A., Nadel, A., Ryvchin, V. (2021). Local Search with a SAT Oracle for Combinatorial Optimization. In: Groote, J.F., Larsen, K.G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science(), vol 12652. Springer, Cham. https://doi.org/10.1007/978-3-030-72013-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-72013-1_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-72012-4
Online ISBN: 978-3-030-72013-1
eBook Packages: Computer ScienceComputer Science (R0)