Abstract
In this paper, we propose the use of path relinking to improve the performance of parallel portfolio-based local search solvers for the Boolean Satisfiability problem. In the portfolio-based framework several algorithms explore the search space in parallel, either independently or cooperatively with some communication between the solvers. Path relinking is a method to maintain an appropriate balance between diversification and intensification (and explore paths that aggregate elite solutions) to properly craft a new assignment for the variables to restart from. We present an empirical study that suggest that path relinking outperforms a set of well-known parallel portfolio-based local search algorithms with and without cooperation.
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.
n denotes the number of variables in the problem.
- 2.
- 3.
Please notice that AG2 only reports two cooperative policies as Prob is the winner strategy.
- 4.
In this paper, we use the implementation of Dist, CCEHC, CCLS, Prob and PNorm available in the SAT competitions and the website of the authors.
References
Arbelaez, A., Codognet, P.: From sequential to parallel local search for SAT. In: Middendorf, M., Blum, C. (eds.) EvoCOP 2013. LNCS, vol. 7832, pp. 157–168. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37198-1_14
Arbelaez, A., Hamadi, Y.: Improving parallel local search for SAT. In: Coello, C.A.C. (ed.) LION 2011. LNCS, vol. 6683, pp. 46–60. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25566-3_4
Arbelaez, A., Hamadi, Y., Sebag, M.: Continuous search in constraint programming. In: Hamadi, Y., Monfroy, E., Saubion, F. (eds.) Autonomous Search, pp. 219–243. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21434-9_9
Birattari, M., Stützle, T., Paquete, L., Varrentrapp, K.: A racing algorithm for configuring metaheuristics. In: GECCO, pp. 11–18 (2002)
Cai, S., Luo, C., Lin, J., Su, K.: New local search methods for partial MaxSAT. Artif. Intell. 240, 1–18 (2016)
Glover, F.: Tabu search for nonlinear and parametric optimization (with links to genetic algorithms). Discrete Appl. Math. 49(1–3), 231–255 (1994)
Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. JSAT 6(4), 245–262 (2009)
Hoos, H.H.: An adaptive noise mechanism for WalkSAT. In: AAAI/IAAI, pp. 655–660 (2002)
Hutter, F., Hoos, H.H., Leyton-Brown, K.: Tradeoffs in the empirical evaluation of competing algorithm designs. Ann. Math. Artif. Intell. 60(1–2), 65–89 (2010)
Hutter, F., Hoos, H.H., Leyton-Brown, K., Stützle, T.: ParamILS: an automatic algorithm configuration framework. J. Artif. Intell. Res. 36, 267–306 (2009)
Li, C.M., Wei, W., Zhang, H.: Combining adaptive noise and look-ahead in local search for SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 121–133. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72788-0_15
Luo, C., Cai, S., Su, K., Huang, W.: CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability. Artif. Intell. 243, 26–44 (2017)
Luo, C., Cai, S., Wu, W., Jie, Z., Su, K.: CCLS: an efficient local search algorithm for weighted maximum satisfiability. IEEE Trans. Comput. 64(7), 1830–1843 (2015)
Martins, R., Manquinho, V.M., Lynce, I.: An overview of parallel SAT solving. Constraints 17(3), 304–347 (2012)
Roli, A.: Criticality and parallelism in structured SAT instances. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 714–719. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46135-3_51
Roli, A., Blesa, M.J., Blum, C.: Random walk and parallelism in local search. In: Metaheuristic International Conference (MIC 2005), Vienna, Austria (2005)
Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: AAAI, pp. 337–343 (1994)
Selman, B., Levesque, H.J., Mitchell, D.G.: A new method for solving hard satisfiability problems. In: AAAI 1996, pp. 440–446 (1996)
Strickland, D.M., Barnes, E.R., Sokol, J.S.: Optimal protein structure alignment using maximum cliques. Oper. Res. 53(3), 389–402 (2005)
Thornton, J., Pham, D.N., Bain, S., Ferreira Jr., V.: Additive versus multiplicative clause weighting for SAT. In: AAAI. pp. 191–196 (2004)
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.) SAT 2004. LNCS, vol. 3542, pp. 306–320. Springer, Heidelberg (2005). https://doi.org/10.1007/11527695_24
Vasquez, M., Hao, J.: A “logic-constrained” knapsack formulation and a tabu algorithm for the daily photograph scheduling of an earth observation satellite. Comput. Optim. Appl. 20(2), 137–157 (2001)
Zhang, L., Bacchus, F.: MAXSAT heuristics for cost optimal planning. In: AAAI 2012 (2012)
Zhang, W., Rangan, A., Looks, M.: Backbone guided local search for maximum satisfiability. In: IJCAI 2003, pp. 1179–1186 (2003)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Jarvis, P., Arbelaez, A. (2020). Cooperative Parallel SAT Local Search with Path Relinking. In: Paquete, L., Zarges, C. (eds) Evolutionary Computation in Combinatorial Optimization. EvoCOP 2020. Lecture Notes in Computer Science(), vol 12102. Springer, Cham. https://doi.org/10.1007/978-3-030-43680-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-43680-3_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-43679-7
Online ISBN: 978-3-030-43680-3
eBook Packages: Computer ScienceComputer Science (R0)