Abstract
In this paper, we present a hybrid optimization architecture which combines on one side incomplete search processes that are often used to quickly find good-quality solutions to large-size problems, and on the other side clause generation techniques that are known to be efficient to boost systematic search. In this architecture, clauses are generated once a locally optimal solution is found. We introduce a generic component to store these clauses generated step-by-step. This component is able to prune neighborhoods by answering queries formulated by the incomplete search process. We define three versions of this clause basis manager and then experiment with an Operations Research problem known as the Orienteering Problem with Time Windows (OPTW) to show the efficiency of the approach.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
Github URL of the source code: https://github.com/thtran97/kb_ls_cpp.
- 3.
- 4.
References
Audemard, G., Lagniez, J.M., Mazure, B., Saïs, L.: Integrating conflict driven clause learning to local search. In: 6th International Workshop on Local Search Techniques in Constraint Satisfaction (LSCS 2009) (2009)
Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309–317. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39071-5_23
Bellman, R.: Dynamic programming treatment of the travelling salesman problem. J. ACM (JACM) 9(1), 61–63 (1962)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. Comput. IEEE Trans. 100(8), 677–691 (1986)
Crawford, J.: Solving satisfiability problems using a combination of systematic and local search. In: Second Challenge on Satisfiability Testing organized by Center for Discrete Mathematics and Computer Science of Rutgers University (1996)
Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17, 229–264 (2002)
Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electron. Notes Theor. Comput. Sci. 89(4), 543–560 (2003)
Gillard, X., Schaus, P.: Large neighborhood search with decision diagrams. In: International Joint Conference on Artificial Intelligence (2022)
Glover, F., Laguna, M.: Tabu search. In: Du, D.Z., Pardalos, P.M. (eds.) Handbook of Combinatorial Optimization, pp. 2093–2229. Springer, Boston (1998). https://doi.org/10.1007/978-1-4613-0303-9_33
Golden, B.L., Levy, L., Vohra, R.: The orienteering problem. Naval Res. Logistics (NRL) 34(3), 307–318 (1987)
Gunawan, A., Lau, H.C., Vansteenwegen, P.: Orienteering problem: a survey of recent variants, solution approaches and applications. Eur. J. Oper. Res. 255(2), 315–332 (2016)
Hentenryck, P.V., Michel, L.: Constraint-Based Local Search. The MIT Press, Cambridge (2005)
Hirsch, E., Kojevnikov, A.: UnitWalk: a new SAT solver that uses local search guided by unit clause elimination. Ann. Math. Artif. Intell. 43, 91–111 (2002)
Hooker, J., Ottosson, G.: Logic-based Benders’ decomposition. Math. Program. Ser. B 96, 33–60 (2003)
Ignatiev, A., Semenov, A.: DPLL+ROBDD derivation applied to inversion of some cryptographic functions. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 76–89. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21581-0_8
Kantor, M.G., Rosenwein, M.B.: The orienteering problem with time windows. J. Oper. Res. Soc. 43(6), 629–635 (1992)
Li, X.Y., Stallmann, M.F., Brglez, F.: QingTing: a fast SAT solver using local search and efficient unit propagation. In: Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2003) (2003)
Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 133–182. IOS Press (2021)
Mazure, B., Sais, L., Grégoire, É.: Boosting complete techniques thanks to local search methods. Ann. Math. Artif. Intell. 22(3), 319–331 (1998)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th annual Design Automation Conference, pp. 530–535 (2001)
Nadel, A., Ryvchin, V.: Efficient SAT solving under assumptions. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 242–255. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31612-8_19
Pesant, G., Gendreau, M.: A constraint programming framework for local search methods. J. Heuristics 5(3), 255–279 (1999)
Pisinger, D., Ropke, S.: Large neighborhood search. In: Gendreau, M., Potvin, J.-Y. (eds.) Handbook of Metaheuristics. ISORMS, vol. 272, pp. 99–127. Springer, Cham (2019). https://doi.org/10.1007/978-3-319-91086-4_4
Prestwich, S.: The relation between complete and incomplete search. In: Blum, C., Aguilera, M.J.B., Roli, A., Sampels, M. (eds.) Hybrid Metaheuristics. Studies in Computational Intelligence, vol. 114, pp. 63–83. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78295-7_3
Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of 1993 International Conference on Computer Aided Design (ICCAD), pp. 42–47. IEEE (1993)
Savelsbergh, M.W.: Local search in routing problems with time windows. Ann. Oper. Res. 4(1), 285–305 (1985)
Schmid, V., Ehmke, J.F.: An effective large neighborhood search for the team orienteering problem with time windows. In: ICCL 2017. LNCS, vol. 10572, pp. 3–18. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68496-3_1
Schutt, A., Feydy, T., Stuckey, P., Wallace, M.: Solving RCPSP/max by lazy clause generation. J. Sched. 16(3), 273–289 (2013)
Solomon, M.M.: Algorithms for the vehicle routing and scheduling problems with time window constraints. Oper. Res. 35(2), 254–265 (1987)
Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: 12th International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 244–257 (2009)
Vansteenwegen, P., Souffriau, W., Berghe, G.V., Van Oudheusden, D.: Iterated local search for the team orienteering problem with time windows. Comput. Oper. Res. 36(12), 3281–3290 (2009)
Vansteenwegen, P., Souffriau, W., Van Oudheusden, D.: The orienteering problem: a survey. Eur. J. Oper. Res. 209(1), 1–10 (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Tran, TH., Pralet, C., Fargier, H. (2023). Combining Incomplete Search and Clause Generation: An Application to the Orienteering Problems with Time Windows. In: Cire, A.A. (eds) Integration of Constraint Programming, Artificial Intelligence, and Operations Research. CPAIOR 2023. Lecture Notes in Computer Science, vol 13884. Springer, Cham. https://doi.org/10.1007/978-3-031-33271-5_32
Download citation
DOI: https://doi.org/10.1007/978-3-031-33271-5_32
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-33270-8
Online ISBN: 978-3-031-33271-5
eBook Packages: Computer ScienceComputer Science (R0)