Document Open Access Logo

UpMax: User Partitioning for MaxSAT

Authors Pedro Orvalho , Vasco Manquinho , Ruben Martins

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.19.pdf
  • Filesize: 0.89 MB
  • 13 pages

Document Identifiers

Author Details

Pedro Orvalho
  • INESC-ID, Instituto Superior Técnico, University of Lisbon, Portugal
Vasco Manquinho
  • INESC-ID, Instituto Superior Técnico, University of Lisbon, Portugal
Ruben Martins
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This work was partially supported by NSF award CCF-1762363 and an Amazon Research Award. This work was also supported by Portuguese national funds through FCT under projects UIDB/50021/2020, PTDC/CCI-COM/2156/2021, 2022.03537.PTDC and grant SFRH/BD/07724/2020, and by project ANI 045917 funded by FEDER and FCT.

Cite AsGet BibTex

Pedro Orvalho, Vasco Manquinho, and Ruben Martins. UpMax: User Partitioning for MaxSAT. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 19:1-19:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.19

Abstract

It has been shown that Maximum Satisfiability (MaxSAT) problem instances can be effectively solved by partitioning the set of soft clauses into several disjoint sets. The partitioning methods can be based on clause weights (e.g., stratification) or based on graph representations of the formula. Afterwards, a merge procedure is applied to guarantee that an optimal solution is found. This paper proposes a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms. As a result, new partitioning procedures can be defined independently of the MaxSAT algorithm to be used. Moreover, this decoupling also allows users that build new MaxSAT formulas to propose partition schemes based on knowledge of the problem to be solved. We illustrate this approach using several problems and show that partitioning has a large impact on the performance of unsatisfiability-based MaxSAT algorithms.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Optimization algorithms
Keywords
  • Maximum Satisfiability
  • Formula partitioning
  • Graph-based methods

Metrics

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

Related Versions

Supplementary Materials

References

  1. https://github.com/forge-lab/upmax. Last accessed on 28th February 2023. URL: https://github.com/forge-lab/upmax.
  2. https://maxsat-evaluations.github.io/2022/. Last accessed on 28th February 2023. URL: https://maxsat-evaluations.github.io/2022/.
  3. C. Ansótegui, Jesús Giráldez-Cru, and Jordi Levy. The Community Structure of SAT Formulas. In International Conference on Theory and Applications of Satisfiability Testing, volume 7317 of LNCS, pages 410-423. Springer, 2012. Google Scholar
  4. Carlos Ansótegui, Maria Luisa Bonet, Joel Gabàs, and Jordi Levy. Improving SAT-Based Weighted MaxSAT Solvers. In Principles and Practice of Constraint Programming, volume 7514 of LNCS, pages 86-101. Springer, 2012. Google Scholar
  5. Carlos Ansótegui, Maria Luisa Bonet, Joel Gabàs, and Jordi Levy. Improving WPM2 for (Weighted) Partial MaxSAT. In Principles and Practice of Constraint Programming, volume 8124 of LNCS, pages 117-132. Springer, 2013. Google Scholar
  6. Carlos Ansótegui and Joel Gabàs. WPM3: an (in)complete algorithm for weighted partial maxsat. Artificial Intelligence, 250:37-57, 2017. Google Scholar
  7. Josep Argelich and Felip Manyà. Exact max-sat solvers for over-constrained problems. J. Heuristics, 12(4-5):375-392, 2006. Google Scholar
  8. Florent Avellaneda. A short description of the solver evalmaxsat. MaxSAT Evaluation, 8, 2020. Google Scholar
  9. Jeremias Berg, Antti Hyttinen, and Matti Järvisalo. Applications of maxsat in data analysis. In Daniel Le Berre and Matti Järvisalo, editors, International Workshop Pragmatics of SAT, volume 59 of EPiC Series in Computing, pages 50-64. EasyChair, 2018. Google Scholar
  10. V.D. Blondel, J.L. Guillaume, R. Lambiotte, and E. Lefebvre. Fast unfolding of communities in large networks. Journal of Statistical Mechanics, 2008(10):P10008, 2008. Google Scholar
  11. Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Jimmy Ho-Man Lee, editor, Principles and Practice of Constraint Programming, volume 6876 of LNCS, pages 225-239. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23786-7_19.
  12. Jessica Davies and Fahiem Bacchus. Exploiting the Power of mip Solvers in maxsat. In International Conference on Theory and Applications of Satisfiability Testing, volume 7962 of LNCS, pages 166-181. Springer, 2013. Google Scholar
  13. Jessica Davies and Fahiem Bacchus. Postponing Optimization to Speed Up MAXSAT Solving. In Christian Schulte, editor, Principles and Practice of Constraint Programming, volume 8124 of LNCS, pages 247-262. Springer, 2013. Google Scholar
  14. Emir Demirovic, Nysret Musliu, and Felix Winter. Modeling and solving staff scheduling with partial weighted maxsat. Annals OR, 275(1):79-99, 2019. URL: https://doi.org/10.1007/s10479-017-2693-y.
  15. Niklas Eén and Niklas Sörensson. Translating Pseudo-Boolean Constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2:1-26, 2006. Google Scholar
  16. Zhaohui Fu and Sharad Malik. On Solving the Partial MAX-SAT Problem. In International Conference on Theory and Applications of Satisfiability Testing, volume 4121 of LNCS, pages 252-265. Springer, 2006. Google Scholar
  17. Federico Heras, António Morgado, and João Marques-Silva. An empirical study of encodings for group maxsat. In Leila Kosseim and Diana Inkpen, editors, Canadian Conference on Artificial Intelligence, volume 7310 of LNCS, pages 85-96. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-30353-1_8.
  18. Toshinori Hosokawa, Hiroshi Yamazaki, Kenichiro Misawa, Masayoshi Yoshimura, Yuki Hirama, and Masavuki Arai. A Low Capture Power Oriented X-filling Method Using Partial MaxSAT Iteratively. In International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems, pages 1-6. IEEE, 2019. Google Scholar
  19. Alexey Ignatiev, António Morgado, and João Marques-Silva. PySAT: A Python Toolkit for Prototyping with SAT Oracles. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, International Conference on Theory and Applications of Satisfiability Testing, volume 10929 of LNCS, pages 428-437. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_26.
  20. Alexey Ignatiev, António Morgado, and João Marques-Silva. RC2: an efficient maxsat solver. J. Satisf. Boolean Model. Comput., 11(1):53-64, 2019. URL: https://doi.org/10.3233/SAT190116.
  21. Daniel Jackson. Software Abstractions: Logic, language, and analysis. MIT Press, 2006. Google Scholar
  22. Mikoláš Janota, Inês Lynce, Vasco Manquinho, and Joao Marques-Silva. PackUp: Tools for Package Upgradability Solving. Journal on Satisfiability, Boolean Modeling and Computation, 8(1/2):89-94, 2012. Google Scholar
  23. Manu Jose and Rupak Majumdar. Cause clue clauses: error localization using maximum satisfiability. In Programming Language Design and Implementation, pages 437-446. ACM, 2011. Google Scholar
  24. Eunsuk Kang, Aleksandar Milicevic, and Daniel Jackson. Multi-representational security analysis. In fse, FSE 2016, pages 181-192. ACM, 2016. Google Scholar
  25. Sarfraz Khurshid and Darko Marinov. Testera: Specification-based testing of java programs using SAT. Autom. Softw. Eng., 11(4):403-434, 2004. Google Scholar
  26. Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa. QMaxSAT: A Partial Max-SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation, 8(1/2):95-100, 2012. URL: https://doi.org/10.3233/sat190091.
  27. Zhendong Lei, Shaowei Cai, Dongxu Wang, Yongrong Peng, Fei Geng, Dongdong Wan, Yiping Deng, and Pinyan Lu. Cashwmaxsat: Solver description. MaxSAT Evaluation, 2021:8, 2021. Google Scholar
  28. Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Combining clause learning and branch and bound for maxsat. In Laurent D. Michel, editor, Principles and Practice of Constraint Programming, volume 210 of LIPIcs, pages 38:1-38:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.38.
  29. Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Boosting branch-and-bound maxsat solvers with clause learning. AI Communications, 35(2):131-151, 2022. Google Scholar
  30. Ferney A. Maldonado-Lopez, Jaime Chavarriaga, and Yezid Donoso. Detecting network policy conflicts using alloy. In Yamine Aït Ameur and Klaus-Dieter Schewe, editors, International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, volume 8477 of LNCS, pages 314-317. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43652-3_31.
  31. Vasco Manquinho, Joao Marques-Silva, and Jordi Planes. Algorithms for Weighted Boolean Optimization. In International Conference on Theory and Applications of Satisfiability Testing, volume 5584 of LNCS, pages 495-508. Springer, 2009. Google Scholar
  32. João Marques-Silva, Josep Argelich, Ana Graça, and Inês Lynce. Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell., 62(3-4):317-343, 2011. URL: https://doi.org/10.1007/s10472-011-9233-2.
  33. João Marques-Silva and Jordi Planes. On Using Unsatisfiability for Solving Maximum Satisfiability. CoRR, 2007. URL: https://arxiv.org/abs/0712.1097.
  34. Ruben Martins, Saurabh Joshi, Vasco Manquinho, and Inês Lynce. Incremental Cardinality Constraints for MaxSAT. In Principles and Practice of Constraint Programming, volume 8656 of LNCS, pages 531-548. Springer, 2014. Google Scholar
  35. Ruben Martins, Vasco Manquinho, and Inês Lynce. On partitioning for maximum satisfiability. In European Conference on Artificial Intelligence, volume 242 of Frontiers in Artificial Intelligence and Applications, pages 913-914. IOS Press, 2012. Google Scholar
  36. Ruben Martins, Vasco Manquinho, and Inês Lynce. Open-WBO: a Modular MaxSAT Solver. In International Conference on Theory and Applications of Satisfiability Testing, volume 8561 of LNCS, pages 438-445. Springer, 2014. Google Scholar
  37. Ruben Martins, Vasco M. Manquinho, and Inês Lynce. Community-based partitioning for maxsat solving. In International Conference on Theory and Applications of Satisfiability Testing, volume 7962 of LNCS, pages 182-191. Springer, 2013. Google Scholar
  38. Erick Moreno-Centeno and Richard M. Karp. The implicit hitting set approach to solve combinatorial optimization problems with an application to multigenome alignment. Oper. Res., 61(2):453-468, 2013. URL: https://doi.org/10.1287/opre.1120.1139.
  39. A. Morgado, F. Heras, M. Liffiton, J. Planes, and J. Marques-Silva. Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints, 18(4):478-534, 2013. Google Scholar
  40. António Morgado, Carmine Dodaro, and João Marques-Silva. Core-Guided MaxSAT with Soft Cardinality Constraints. In Principles and Practice of Constraint Programming, volume 8656 of LNCS, pages 564-573. Springer, 2014. Google Scholar
  41. António Morgado, Alexey Ignatiev, and João Marques-Silva. MSCG: robust core-guided maxsat solving. J. Satisf. Boolean Model. Comput., 9(1):129-134, 2014. URL: https://doi.org/10.3233/sat190105.
  42. Miguel Neves, Ruben Martins, Mikolás Janota, Inês Lynce, and Vasco Manquinho. Exploiting resolution-based representations for maxsat solving. In Marijn Heule and Sean A. Weaver, editors, International Conference on Theory and Applications of Satisfiability Testing, volume 9340 of LNCS, pages 272-286. Springer, 2015. Google Scholar
  43. Pedro Orvalho, Vasco Manquinho, and Ruben Martins. Upmax: User partitioning for maxsat, 2023. URL: https://arxiv.org/abs/2305.16191.
  44. Tobias Paxian, Sven Reimer, and Bernd Becker. Dynamic polynomial watchdog encoding for solving weighted maxsat. In International Conference on Theory and Applications of Satisfiability Testing, volume 10929 of LNCS, pages 37-53. Springer, 2018. Google Scholar
  45. Marek Piotrów. UWrMaxSat - a new MiniSat+ - based Solver in MaxSAT Evaluation 2019. MaxSAT Evaluation 2019 : Solver and Benchmark Descriptions, B-2019-2:11, 2019. Google Scholar
  46. Marek Piotrów. UWrMaxSat: Efficient Solver for MaxSAT and Pseudo-Boolean Problems. In International Conference on Tools with Artificial Intelligence, pages 132-136. IEEE, 2020. Google Scholar
  47. Paul Saikko, Jeremias Berg, and Matti Järvisalo. LMHS: A SAT-IP hybrid maxsat solver. In International Conference on Theory and Applications of Satisfiability Testing, volume 9710 of LNCS, pages 539-546. Springer, 2016. Google Scholar
  48. Aaron Stump, Geoff Sutcliffe, and Cesare Tinelli. Starexec: A cross-community infrastructure for logic solving. In International Joint Conference on Automated Reasoning, volume 8562 of LNCS, pages 367-373. Springer, 2014. Google Scholar
  49. Caroline Trippel, Daniel Lustig, and Margaret Martonosi. CheckMate: Automated synthesis of hardware exploits and security litmus tests. Proceedings of the Annual International Symposium on Microarchitecture, MICRO, 2018-Octob:947-960, 2018. Google Scholar
  50. Allen Van Gelder. Variable independence and resolution paths for quantified boolean formulas. In Principles and Practice of Constraint Programming, volume 6876 of LNCS, pages 789-803. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23786-7_59.
  51. Rouven Walter, Christoph Zengler, and Wolfgang Küchlin. Applications of maxsat in automotive configuration. In International Configuration Workshop, volume 1128 of CEUR Workshop Proceedings, pages 21-28. CEUR-WS.org, 2013. Google Scholar
  52. Robert A. Yates, Bertram Raphael, and Timothy P. Hart. Resolution graphs. Artificial Intelligence, 1(4):257-289, 1970. URL: https://doi.org/10.1016/0004-3702(70)90011-1.
  53. Aolong Zha, Miyuki Koshimura, and Hiroshi Fujita. N-level modulo-based CNF encodings of pseudo-boolean constraints for maxsat. Constraints An Int. J., 24(2):133-161, 2019. URL: https://doi.org/10.1007/s10601-018-9299-0.
  54. Changjian Zhang, Ryan Wagner, Pedro Orvalho, David Garlan, Vasco Manquinho, Ruben Martins, and Eunsuk Kang. AlloyMax: bringing maximum satisfaction to relational specifications. In Diomidis Spinellis, Georgios Gousios, Marsha Chechik, and Massimiliano Di Penta, editors, fse, pages 155-167. ACM, 2021. Google Scholar
  55. Lei Zhang and Fahiem Bacchus. MAXSAT heuristics for cost optimal planning. In AAAI Conference on Artificial Intelligence. AAAI Press, 2012. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI12/paper/view/5190.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact