Document Open Access Logo

LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem

Authors Junping Zhou , Jiaxin Liang , Minghao Yin , Bo He

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2023.29.pdf
  • Filesize: 1.04 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Random search heuristics
  • Theory of computation → Constraint and logic programming
Keywords
  • Top-k
  • MaxSAT
  • local search

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

The Maximum Satisfiability (MaxSAT), an important optimization problem, has a range of applications, including network routing, planning and scheduling, and combinatorial auctions. Among these applications, one usually benefits from having not just one single solution, but k diverse solutions. Motivated by this, we study an extension of MaxSAT, named Diversified Top-k MaxSAT (DTKMS) problem, which is to find k feasible assignments of a given formula such that each assignment satisfies all hard clauses and all of them together satisfy the maximum number of soft clauses. This paper presents a local search algorithm, LS-DTKMS, for DTKMS problem, which exploits novel scoring functions to select variables and assignments. Experiments demonstrate that LS-DTKMS outperforms the top-k MaxSAT based DTKMS solvers and state-of-the-art solvers for diversified top-k clique problem.

Cite As Get BibTex

Junping Zhou, Jiaxin Liang, Minghao Yin, and Bo He. LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.SAT.2023.29

Author Details

Junping Zhou
  • School of Information Science and Technology, Northeast Normal University, Changchun, China
Jiaxin Liang
  • School of Information Science and Technology, Northeast Normal University, Changchun, China
Minghao Yin
  • School of Information Science and Technology, Northeast Normal University, Changchun, China
  • Key Laboratory of Applied Statistics of MOE, Northeast Normal University, Changchun, China
Bo He
  • School of Information Science and Technology, Northeast Normal University, Changchun, China

Funding

This work is supported by Science and Technology Development Program of Jilin Province (20230101060JC and YDZJ202201ZYTS412), NSFC (under Grant No.61976050, 61972384), the Fundamental Research Funds for the Central Universities 2412019ZD013, and Jilin Science and Technology Department 20200201280JC.

Acknowledgements

We would like to thank all the anonymous reviewers for their helpful comments.

Supplementary Materials

References

  1. Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael Lifshits, and Alexander Nadel. Sat-based semiformal verification of hardware. In Roderick Bloem and Natasha Sharygina, editors, Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23, pages 25-32. IEEE, 2010. URL: https://doi.org/10.5555/1998496.1998505.
  2. Josep Alòs, Carlos Ansótegui, and Eduard Torres. Interpretable decision trees through MaxSAT. Artificial Intelligence Review, pages 1-21, 2022. URL: https://doi.org/10.1007/s10462-022-10377-0.
  3. Mario Alviano. Maxino. MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, pages 21-22, 2020. Google Scholar
  4. Josep Argelich, Chu Min Li, Felip Manyà, and Zhu Zhu. MinSAT versus MaxSAT for optimization problems. In Christian Schulte, editor, Principles and Practice of Constraint Programming - 19th International Conference, CP 2013, Uppsala, Sweden, September 16-20, 2013. Proceedings, volume 8124 of Lecture Notes in Computer Science, pages 133-142. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40627-0_13.
  5. Giorgio Ausiello, Nicolas Boria, Aristotelis Giannakos, Giorgio Lucarelli, and Vangelis Th. Paschos. Online maximum k-coverage. Discrete Applied Mathematics, 160(13-14):1901-1913, 2012. URL: https://doi.org/10.1016/j.dam.2012.04.005.
  6. Fahiem Bacchus. MaxHS in the 2020 MaxSAT evaluation. MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, pages 19-20, 2020. Google Scholar
  7. Hamid Ahmadi Beni and Asgarali Bouyer. TI-SC: top-k influential nodes selection based on community detection and scoring criteria in social networks. Journal of Ambient Intelligence and Humanized Computing, 11(11):4889-4908, 2020. URL: https://doi.org/10.1007/s12652-020-01760-2.
  8. Jeremias Berg and Matti Järvisalo. Optimal correlation clustering via MaxSAT. In Wei Ding, Takashi Washio, Hui Xiong, George Karypis, Bhavani Thuraisingham, Diane J. Cook, and Xindong Wu, editors, 13th IEEE International Conference on Data Mining Workshops, ICDM Workshops, TX, USA, December 7-10, 2013, pages 750-757. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/ICDMW.2013.99.
  9. Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, António Morgado, and João Marques-Silva. Propositional proof systems based on maximum satisfiability. Artificial Intelligence, 300:103552, 2021. URL: https://doi.org/10.1016/j.artint.2021.103552.
  10. Shaowei Cai. Balance between complexity and quality: Local search for minimum vertex cover in massive graphs. In Qiang Yang and Michael J. Wooldridge, editors, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 747-753. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/111.
  11. Shaowei Cai and Zhendong Lei. Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability. Artificial Intelligence, 287:103354, 2020. URL: https://doi.org/10.1016/j.artint.2020.103354.
  12. Mohamed Sami Cherif, Djamal Habet, and André Abramé. Understanding the power of max-sat resolution through up-resilience. Artificial Intelligence, 289:103397, 2020. URL: https://doi.org/10.1016/j.artint.2020.103397.
  13. Rafael Dutra, Kevin Laeufer, Jonathan Bachrach, and Koushik Sen. Efficient sampling of SAT solutions for testing. In Michel Chaudron, Ivica Crnkovic, Marsha Chechik, and Mark Harman, editors, Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27 - June 03, 2018, pages 549-559. ACM, 2018. URL: https://doi.org/10.1145/3180155.3180248.
  14. Wenfei Fan, Xin Wang, and Yinghui Wu. Diversified top-k graph pattern matching. Proceedings of the VLDB Endowment, 6(13):1510-1521, 2013. URL: https://doi.org/10.14778/2536258.2536263.
  15. Kevin Gimpel, Dhruv Batra, Chris Dyer, and Gregory Shakhnarovich. A systematic exploration of diversity in machine translation. In Proceedings of the 2013 Conference on Empirical Methods in Natural Language Processing, EMNLP 2013, 18-21 October 2013, Grand Hyatt Seattle, Seattle, Washington, USA, A meeting of SIGDAT, a Special Interest Group of the ACL, pages 1100-1111. ACL, 2013. URL: https://aclanthology.org/D13-1111/.
  16. Fei Hao, Zheng Pei, and Laurence T. Yang. Diversified top-k maximal clique detection in Social Internet of Things. Future Generation Computer Systems, 107:408-417, 2020. URL: https://doi.org/10.1016/j.future.2020.02.023.
  17. Hao Hu, Marie-José Huguet, and Mohamed Siala. Optimizing binary decision diagrams with MaxSAT for classification. In Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022, pages 3767-3775. AAAI Press, 2022. URL: https://doi.org/10.1609/aaai.v36i4.20291.
  18. Alexey Ignatiev. RC2-2018@ MaxSAT evaluation 2020. MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, pages 13-14, 2020. Google Scholar
  19. Alexey Ignatiev, Yacine Izza, Peter J. Stuckey, and João Marques-Silva. Using MaxSAT for efficient explanations of tree ensembles. In Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022, pages 3776-3785. AAAI Press, 2022. URL: https://doi.org/10.1609/aaai.v36i4.20292.
  20. Mohit Kumar, Samuel Kolb, Stefano Teso, and Luc De Raedt. Learning MAX-SAT from contextual examples for combinatorial optimisation. In Proceedings of the 34th AAAI Conference on Artificial Intelligence, AAAI 2020, pages 4493-4500. AAAI Press, 2020. URL: https://doi.org/10.1609/aaai.v34i04.5877.
  21. Zhendong Lei and Shaowei Cai. Solving (weighted) partial maxsat by dynamic local search for SAT. In Jérôme Lang, editor, Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 1346-1352. ijcai.org, 2018. URL: https://doi.org/10.24963/ijcai.2018/187.
  22. Chu Min Li and Zhe Quan. An efficient branch-and-bound algorithm based on MaxSAT for the maximum clique problem. In Maria Fox and David Poole, editors, Proceedings of the 24th AAAI Conference on Artificial Intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11-15, 2010. AAAI Press, 2010. URL: https://doi.org/10.1609/aaai.v24i1.7536.
  23. Longlong Lin, Pingpeng Yuan, Rong-Hua Li, and Hai Jin. Mining diversified top-r lasting cohesive subgraphs on temporal networks. IEEE Transactions on Big Data, 8(6):1537-1549, 2022. URL: https://doi.org/10.1109/TBDATA.2021.3058294.
  24. Huiping Liu, Cheqing Jin, Bin Yang, and Aoying Zhou. Finding top-k shortest paths with diversity. IEEE Transactions on Knowledge and Data Engineering, 30(3):488-502, 2018. URL: https://doi.org/10.1109/TKDE.2017.2773492.
  25. Bingqing Lyu, Lu Qin, Xuemin Lin, Ying Zhang, Zhengping Qian, and Jingren Zhou. Maximum and top-k diversified biclique search at scale. The VLDB Journal, 31(6):1365-1389, 2022. URL: https://doi.org/10.1007/s00778-021-00681-6.
  26. Ruben Martins, Norbert Manthey, Miguel Terra-Neves, Vasco Manquinho, and Inês Lynce. Open-WBO@ MaxSAT evaluation 2020. MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, pages 24-25, 2020. Google Scholar
  27. Christian J. Muise, Sheila A. McIlraith, and J. Christopher Beck. Optimally relaxing partial-order plans with MaxSAT. In Lee McCluskey, Brian Charles Williams, José Reinaldo Silva, and Blai Bonet, editors, Proceedings of the 22nd International Conference on Automated Planning and Scheduling, ICAPS 2012, Atibaia, São Paulo, Brazil, June 25-19, 2012. AAAI, 2012. URL: https://doi.org/10.1609/icaps.v22i1.13537.
  28. Alexander Nadel. Generating diverse solutions in SAT. In Karem A. Sakallah and Laurent Simon, editors, Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings, volume 6695 of Lecture Notes in Computer Science, pages 287-301. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21581-0_23.
  29. Daniel Cosmin Porumbel, Jin-Kao Hao, and Pascale Kuntz. An efficient algorithm for computing the distance between close partitions. Discrete Applied Mathematics, 159(1):53-59, 2011. URL: https://doi.org/10.1016/j.dam.2010.09.002.
  30. Daniel Cosmin Porumbel, Jin-Kao Hao, and Pascale Kuntz. Spacing memetic algorithms. In Natalio Krasnogor and Pier Luca Lanzi, editors, 13th Annual Genetic and Evolutionary Computation Conference, GECCO 2011, Proceedings, Dublin, Ireland, July 12-16, 2011, pages 1061-1068. ACM, 2011. URL: https://doi.org/10.1145/2001576.2001720.
  31. Caleb Voss, Mark Moll, and Lydia E. Kavraki. A heuristic approach to finding diverse short paths. In IEEE International Conference on Robotics and Automation, ICRA 2015, Seattle, WA, USA, 26-30 May, 2015, pages 4173-4179. IEEE, 2015. URL: https://doi.org/10.1109/ICRA.2015.7139774.
  32. Jun Wu, Chu-Min Li, Lu Jiang, Junping Zhou, and Minghao Yin. Local search for diversified top-k clique search problem. Computers & Operations Research, 116:104867, 2020. URL: https://doi.org/10.1016/j.cor.2019.104867.
  33. Jun Wu, Chu-Min Li, Luzhi Wang, Shuli Hu, Peng Zhao, and Minghao Yin. On solving simplified diversified top-k s-plex problem. Computers & Operations Research, 153:106187, 2023. URL: https://doi.org/10.1016/j.cor.2023.106187.
  34. Jun Wu, Chu-Min Li, Yupeng Zhou, Minghao Yin, Xin Xu, and Dangdang Niu. HEA-D: A hybrid evolutionary algorithm for diversified top-k weight clique search problem. In Lud De Raedt, editor, Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022, pages 4821-4827. International Joint Conferences on Artificial Intelligence Organization, July 2022. URL: https://doi.org/10.24963/ijcai.2022/668.
  35. Mingyu Xiao. An exact MaxSAT algorithm: Further observations and further improvements. In Luc De Raedt, editor, Proceedings of the 31st International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022, pages 1887-1893. ijcai.org, 2022. URL: https://doi.org/10.24963/ijcai.2022/262.
  36. Hongfei Xu, Yu Gu, Jianzhong Qi, Jiayuan He, and Ge Yu. Diversifying top-k routes with spatial constraints. Journal of Computer Science and Technology, 34(4):818-838, 2019. URL: https://doi.org/10.1007/s11390-019-1944-6.
  37. Long Yuan, Lu Qin, Xuemin Lin, Lijun Chang, and Wenjie Zhang. Diversified top-k clique search. The VLDB Journal, 25(2):171-196, 2016. URL: https://doi.org/10.1007/s00778-015-0408-z.
  38. Xiaoqi Zheng, Taigang Liu, Zhongnan Yang, and Jun Wang. Large cliques in arabidopsis gene coexpression network and motif discovery. Journal of plant physiology, 168(6):611-618, 2011. URL: https://doi.org/10.1016/j.jplph.2010.09.010.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact