Abstract
Many problems from industrial applications and AI can be encoded as Maximum Satisfiability (MaxSAT). Often, it is more desirable to produce practicable results in very short time compared to optimal solutions after an arbitrary long computation time. In this paper, we propose Stable Resolving (SR), a novel randomized local search heuristic for MaxSAT with that aim. SR works for both weighted and unweighted instances. Starting from a feasible initial solution, the algorithm repeatedly performs the three steps of perturbation, improvements and solution checking. In the perturbation, the search space is explored at the cost of possibly worsening the current solution. The local improvements work by repeatedly flipping signs of variables in over-satisfied clauses. Finally, the algorithm performs a solution checking in a simulated annealing fashion. We compare our approach to state-of-the-art MaxSAT solvers and show by numerical experiments on benchmark instances from the annual MaxSAT competition that SR performs comparable on average and is even the best solver for particular problem instances.
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.
We have submitted SR to the 2020’s MaxSAT competition.
References
MaxSAT Evaluation 2019. https://maxsat-evaluations.github.io/2019/index.html
Starexec Cluster. https://www.starexec.org/starexec/public/about.jsp. Accessed 2019
Andrade, D.V., Resende, M.G.C., Werneck, R.F.F.: Fast local search for the maximum independent set problem. J. Heuristics 18(4), 525–547 (2012). https://doi.org/10.1007/s10732-012-9196-4
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, San Francisco, CA, USA, pp. 399–404 (2009)
Bacchus, F., Järvisalo, M., Martins, R.: MaxSAT evaluation 2018: new developments and detailed results. J. Satisf. Boolean Model. Comput. 11, 99–131 (2019). https://doi.org/10.3233/SAT190119
Belov, A., Morgado, A., Marques-Silva, J.: SAT-based preprocessing for MaxSAT. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 96–111. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_7
Berg, J., Demirović, E., Stuckey, P.J.: Core-boosted linear search for incomplete MaxSAT. In: Rousseau, L.-M., Stergiou, K. (eds.) CPAIOR 2019. LNCS, vol. 11494, pp. 39–56. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-19212-9_3
Berg, J., Järvisalo, M.: Cost-optimal constrained correlation clustering via weighted partial maximum satisfiability. Artif. Intell. 244, 110–142 (2017). https://doi.org/10.1016/j.artint.2015.07.001. Combining Constraint Solving with Mining and Learning
Berg, J., Järvisalo, M., Malone, B.: Learning optimal bounded treewidth Bayesian networks via maximum satisfiability. In: Kaski, S., Corander, J. (eds.) Proceedings of the Seventeenth International Conference on Artificial Intelligence and Statistics. Proceedings of Machine Learning Research, vol. 33, pp. 86–95. PMLR, Reykjavik, 22–25 April 2014
Bouhmala, N.: Combining simulated annealing with local search heuristic for Max-SAT. J. Heuristics 25(1), 47–69 (2019). https://doi.org/10.1007/s10732-018-9386-9
Dantzig, G.B.: Linear Programming and Extensions. Princeton University Press, Princeton (1963)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960). https://doi.org/10.1145/321033.321034
Demirović, E., Stuckey, P.J.: Techniques inspired by local search for incomplete MaxSAT and the linear algorithm: varying resolution and solution-guided search. In: Schiex, T., de Givry, S. (eds.) CP 2019. LNCS, vol. 11802, pp. 177–194. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30048-7_11
Fan, Y., Ma, Z., Su, K., Sattar, A., Li, C.: Ramp: a local search solver based on make-positive variables. In: MaxSAT Evaluation (2016)
Großmann, P., Hölldobler, S., Manthey, N., Nachtigall, K., Opitz, J., Steinke, P.: Solving periodic event scheduling problems with SAT. In: Jiang, H., Ding, W., Ali, M., Wu, X. (eds.) IEA/AIE 2012. LNCS (LNAI), vol. 7345, pp. 166–175. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31087-4_18
Guerra, J., Lynce, I.: Reasoning over biological networks using maximum satisfiability. In: Milano, M. (ed.) CP 2012. LNCS, pp. 941–956. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33558-7_67
Hoos, H.H.: Solving hard combinatorial problems with GSAT—A case study. In: Görz, G., Hölldobler, S. (eds.) KI 1996. LNCS, vol. 1137, pp. 107–119. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61708-6_53
Hyttinen, A., Eberhardt, F., Järvisalo, M.: Constraint-based causal discovery: conflict resolution with answer set programming. In: Proceedings of the 30th Conference on Uncertainty in Artificial Intelligence, pp. 340–349 (2014)
Lei, Z., Cai, S.: Solving (weighted) partial MaxSAT by dynamic local search for sat. In: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, pp. 1346–1352. International Joint Conferences on Artificial Intelligence Organization, July 2018. https://doi.org/10.24963/ijcai.2018/187
Park, J.D.: Using weighted Max-SAT engines to solve MPE. In: Proceedings of the 18th National Conference on Artificial Intelligence, pp. 682–687 (2002)
Pisinger, D., Ropke, S.: Large neighborhood search. In: Gendreau, M., Potvin, J.Y. (eds.) Handbook of Metaheuristics. International Series in Operations Research & Management Science, vol. 146, pp. 399–419. Springer, Boston (2010). https://doi.org/10.1007/978-1-4419-1665-5_13
Reisch, J., Großmann, P., Kliewer, N.: Conflict resolving - a maximum independent set heuristics for solving MaxSAT. In: Proceedings of the 22nd International Multiconference Information Society, vol. 1, pp. 67–71 (2019)
Selman, B., Kautz, H., Cohen, B.: Local search strategies for satisfiability testing. In: DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pp. 521–532 (1995)
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
Reisch, J., Großmann, P., Kliewer, N. (2020). Stable Resolving - A Randomized Local Search Heuristic for MaxSAT. In: Schmid, U., Klügl, F., Wolter, D. (eds) KI 2020: Advances in Artificial Intelligence. KI 2020. Lecture Notes in Computer Science(), vol 12325. Springer, Cham. https://doi.org/10.1007/978-3-030-58285-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-030-58285-2_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-58284-5
Online ISBN: 978-3-030-58285-2
eBook Packages: Computer ScienceComputer Science (R0)