Parallel Maximum Satisfiability

Chapter

Abstract

Developments in parallel Boolean Satisfiability (SAT) have motivated developments in parallel Maximum Satisfiability (MaxSAT), where MaxSAT is the optimization counterpart of SAT. Although many of the techniques implemented in parallel SAT can be extended to parallel MaxSAT, additional techniques are required to deal with the optimization part. This chapter provides an overview of the state of the art in parallel Maximum Satisfiability. The required background is first provided, namely the characteristics of the different MaxSAT algorithms. Solutions to parallel MaxSAT solving include portfolio approaches and search space splitting. Clause sharing is a key issue and so conditions for safe clause sharing are described. Deterministic parallel MaxSAT is another contribution in the field, having the additional challenge of synchronization strategies. Finally, future research directions are discussed.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Notes

Acknowledgments

This work was supported by national funds through Fundação para a Ciência e a Tecnologia (FCT) with reference UID/CEC/50021/2013.

References

  1. [1]
    Achá, R.J.A., Nieuwenhuis, R.: Curriculum-based course timetabling with SAT and MaxSAT. Annals of Operations Research 218(1), 71–91 (2014)Google Scholar
  2. [2]
    An, X., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: A Partial Max-SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation 8, 95–100 (2012)Google Scholar
  3. [3]
    Ansótegui, C., Bonet, M.L., Gabàs, J., Levy, J.: Improving WPM2 for (Weighted) Partial MaxSAT. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 117–132. Springer (2013)Google Scholar
  4. [4]
    Ansótegui, C., Bonet, M.L., Levy, J.: On Solving MaxSAT Through SAT. In: Proc. International Conference of the Catalan Association for Artificial Intelligence, pp. 284–292. IOS Press (2009)Google Scholar
  5. [5]
    Ansótegui, C., Bonet, M.L., Levy, J.: Solving (Weighted) Partial MaxSAT through Satisfiability Testing. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 427–440. Springer (2009)Google Scholar
  6. [6]
    Ansótegui, C., Bonet, M.L., Levy, J.: A New Algorithm for Weighted Partial MaxSAT. In: Proc. AAAI Conference on Artificial Intelligence, pp. 3–8. AAAI Press (2010)Google Scholar
  7. [7]
    Ansótegui, C., Gabàs, J.: Solving (Weighted) Partial MaxSAT with ILP. In: Proc. International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, pp. 403–409. Springer (2013)Google Scholar
  8. [8]
    Ansótegui, C., Manyà, F.: Mapping problems with finite-domain variables into problems with Boolean variables. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 1–15. Springer (2004)Google Scholar
  9. [9]
    Argelich, J., Berre, D.L., Lynce, I., Marques-Silva, J., Rapicault, P.: Solving Linux Upgradeability Problems Using Boolean Optimization. In: Workshop on Logics for Component Configuration, pp. 11–22. Conference Proceedings (2010)Google Scholar
  10. [10]
    Argelich, J., Li, C.M., Manyà, F.: An improved exact solver for Partial Max-SAT. In: Proc. of the International Conference on Nonconvex Programming: Local and Global Approaches, pp. 230–231. Conference Proceedings (2007)Google Scholar
  11. [11]
    Argelich, J., Manyà, F.: Partial Max-SAT Solvers with Clause Learning. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 28–40. Springer (2007)Google Scholar
  12. [12]
    Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality Networks: a theoretical and empirical study. Constraints 16(2), 195–221 (2011)Google Scholar
  13. [13]
    Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.M., Piette, C.: Revisiting Clause Exchange in Parallel SAT Solving. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 200–213. Springer (2012)Google Scholar
  14. [14]
    Audemard, G., Lagniez, J.M., Mazure, B., Sais, L.: On Freezing and Reactivating Learnt Clauses. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 188–200. Springer (2011)Google Scholar
  15. [15]
    Audemard, G., Simon, L.: Predicting Learnt Clauses Quality in Modern SAT Solvers. In: Proc. International Joint Conferences on Artificial Intelligence, pp. 399–404. IJCAI/AAAI Press (2009)Google Scholar
  16. [16]
    Bailleux, O., Boufkhad, Y.: Efficient CNF Encoding of Boolean Cardinality Constraints. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 108–122. Springer (2003)Google Scholar
  17. [17]
    Bailleux, O., Boufkhad, Y., Roussel, O.: New Encodings of Pseudo-Boolean Constraints into CNF. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 181–194. Springer (2009)Google Scholar
  18. [18]
    Berre, D.L., Parrain, A.: The Sat4j library, release 2.2. JSAT 7(2-3), 59–6 (2010)Google Scholar
  19. [19]
    Bjørner, N., Phan, A., Fleckenstein, L.: \( {\nu Z} \) - An Optimizing SMT Solver. In: Proc. Tools and Algorithms for Construction and Analysis of Systems, pp. 194–199. Springer (2015)Google Scholar
  20. [20]
    Böhm, M., Speckenmeyer, E.: A Fast Parallel SAT-Solver - Efficient Workload Balancing. Annals of Mathematics and Artificial Intelligence 17, 381–400 (1996)Google Scholar
  21. [21]
    Bonet, M.L., Levy, J., Manyà, F.: Resolution for Max-SAT. Artificial Intelligence 171(8–9), 606–618 (2007)Google Scholar
  22. [22]
    Chen, Y., Safarpour, S., Marques-Silva, J., Veneris, A.G.: Automated Design Debugging With Maximum Satisfiability. IEEE Transactions on CAD of Integrated Circuits and Systems 29(11), 1804–1817 (2010)Google Scholar
  23. [23]
    Darras, S., Dequen, G., Devendevill, L., Li, C.M.: On Inconsistent Clause-Subsets for Max-SAT Solving. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 225–240. Springer (2007)Google Scholar
  24. [24]
    Davies, J., Bacchus, F.: Solving MAXSAT by Solving a Sequence of Simpler SAT Instances. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 225–239. Springer (2011)Google Scholar
  25. [25]
    Davies, J., Bacchus, F.: Postponing optimization to speed up MAXSAT solving. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 247–262. Springer (2013)Google Scholar
  26. [26]
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 502–518. Springer (2003)Google Scholar
  27. [27]
    Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science 89(4), 543–560 (2003)Google Scholar
  28. [28]
    Eén, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2, 1–26 (2006)Google Scholar
  29. [29]
    Feng, Y., Bastani, O., Martins, R., Dillig, I., Anand, S.: Automated Synthesis of Semantic Malware Signatures using Maximum Satisfiability. In: Network and Distributed System Security Symposium. The Internet Society (2017)Google Scholar
  30. [30]
    Frisch, A.M., Peugniez, T.J., Doggett, A.J., Nightingale, P.: Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings. Journal of Automated Reasoning 35(1-3), 143–179 (2005)Google Scholar
  31. [31]
    Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 252–265. Springer (2006)Google Scholar
  32. [32]
    Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman (1979)Google Scholar
  33. [33]
    Gent, I.P., Nightingale, P.: A new encoding of All Different into SAT. In: International Workshop on Modelling and Reformulating Constraint Satisfaction Problems. Conference Proceedings (2004)Google Scholar
  34. [34]
    Graça, A., Lynce, I., Marques-Silva, J., Oliveira, A.L.: Efficient and Accurate Haplotype Inference by Combining Parsimony and Pedigree Information. In: Algebraic and Numeric Biology, pp. 38–56. Springer (2010)Google Scholar
  35. [35]
    Hamadi, Y., Jabbour, S., Piette, C., Sais, L.: Deterministic Parallel DPLL. Journal on Satisfiability, Boolean Modeling and Computation 7(4), 127–132 (2011)Google Scholar
  36. [36]
    Hamadi, Y., Jabbour, S., Sais, L.: Control-Based Clause Sharing in Parallel SAT Solving. In: Proc. International Joint Conferences on Artificial Intelligence, pp. 499–504. IJCAI/AAAI Press (2009)Google Scholar
  37. [37]
    Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a Parallel SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation 6(4), 245–262 (2009)Google Scholar
  38. [38]
    Heras, F., Morgado, A., Marques-Silva, J.: Core-Guided Binary Search Algorithms for Maximum Satisfiability. In: Proc. AAAI Conference on Artificial Intelligence, pp. 36–41. AAAI Press (2011)Google Scholar
  39. [39]
    Heule, M.J., Kullmann, O.,Wieringa, S., Biere, A.: Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. In: Hardware and Software: Verification and Testing, pp. 50–65. Springer (2012)Google Scholar
  40. [40]
    Hölldobler, S., Manthey, N., Steinke, P.: A compact encoding of pseudo-Boolean constraints into SAT. In: KI 2013: Advances in Artificial Intelligence, pp. 107–118. Springer (2012)Google Scholar
  41. [41]
    Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Proc. Conference on Programming Language Design and Implementation, pp. 437–446. ACM Press (2011)Google Scholar
  42. [42]
    Joshi, S., Martins, R., Manquinho, V.: Generalized Totalizer Encoding for Pseudo-Boolean Constraints. In: International Conference on Principles and Practice of Constraint Programming, pp. 200–209. Springer (2015)Google Scholar
  43. [43]
    Klieber, W., Kwon, G.: Efficient CNF Encoding for Selecting 1 from N Objects. In: International Workshop on Constraints in Formal Verification. Conference Proceedings (2007)Google Scholar
  44. [44]
    Li, C.M., Manyà, F.: MaxSAT, Hard and Soft Constraints. In: Handbook of Satisfiability, pp. 613–631. IOS Press (2009)Google Scholar
  45. [45]
    Li, C.M., Manyà, F., Planes, J.: Exploiting unit propagation to compute lower bounds in branch and bound Max-SAT solvers. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 403–414. Springer (2005)Google Scholar
  46. [46]
    Li, C.M., Manyà, F., Planes, J.: New inference rules for Max-SAT. Journal of Artificial Intelligence Research 30, 321–359 (2007)Google Scholar
  47. [47]
    Lin, H., Su, K.: Exploiting inference rules to compute lower bounds for MAXSAT solving. In: Proc. International Joint Conferences on Artificial Intelligence, pp. 2334–2339. IJCAI/AAAI Press (2007)Google Scholar
  48. [48]
    Lin, H., Su, K., Li, C.M.: Within-problem Learning for Efficient Lower Bound Computation in Max-SAT Solving. In: Proc. AAAI Conference on Artificial Intelligence, pp. 351–356. AAAI Press (2008)Google Scholar
  49. [49]
    Mancinelli, F., Boender, J., Cosmo, R.D., Vouillon, J., Durak, B., Leroy, X., Treinen, R.: Managing the Complexity of Large Free and Open Source Package-Based Software Distributions. In: Proc. International Conference on Automated Software Engineering, pp. 199–208. IEEE Computer Society Press (2006)Google Scholar
  50. [50]
    Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for Weighted Boolean Optimization. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 495–508. Springer (2009)Google Scholar
  51. [51]
    Manquinho, V., Martins, R., Lynce, I.: Improving Unsatisfiability-Based Algorithms for Boolean Optimization. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 181–193. Springer (2010)Google Scholar
  52. [52]
    Marques-Silva, J., Planes, J.: On using unsatisfiability for solving maximum satisfiability. CoRR. http://arXiv.org/abs/0712.1097 (2007)
  53. [53]
    Marques-Silva, J., Sakallah, K.: GRASP: A New Search Algorithm for Satisfiability. In: Proc. International Conference on Computer-Aided Design, pp. 220–227. IEEE Computer Society Press (1996)Google Scholar
  54. [54]
    Marques-Silva, J., Sakallah, K.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers 48(5), 506–521 (1999)Google Scholar
  55. [55]
    Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental Cardinality Constraints for MaxSAT. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 531–548. Springer (2014)Google Scholar
  56. [56]
    Martins, R., Joshi, S., Manquinho, V., Lynce, I.: On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving. Journal on Satisfiability, Boolean Modeling and Computation 9, 59–81 (2015)Google Scholar
  57. [57]
    Martins, R., Manquinho, V., Lynce, I.: Exploiting Cardinality Encodings in Parallel Maximum Satisfiability. In: Proc. International Conference on Tools with Artificial Intelligence, pp. 313–320. IEEE Computer Society Press (2011)Google Scholar
  58. [58]
    Martins, R., Manquinho, V., Lynce, I.: Clause Sharing in Deterministic Parallel Maximum Satisfiability. In: RCRA International Workshop on Experimental Evaluation of Algorithms for solving problems with combinatorial explosion. Conference Proceedings (2012)Google Scholar
  59. [59]
    Martins, R., Manquinho, V., Lynce, I.: Clause Sharing in Parallel MaxSAT. In: Proc. Learning and Intelligent Optimization Conference, pp. 455–460. Springer (2012)Google Scholar
  60. [60]
    Martins, R., Manquinho, V., Lynce, I.: On Partitioning for Maximum Satisfiability. In: Proc. European Conference on Artificial Intelligence, pp. 913–914. IOS Press (2012)Google Scholar
  61. [61]
    Martins, R., Manquinho, V., Lynce, I.: Parallel Search for Maximum Satisfiability. AI Communications 25(2), 75–95 (2012)Google Scholar
  62. [62]
    Martins, R., Manquinho, V., Lynce, I.: Community-based Partitioning for MaxSAT Solving. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 182–191. Springer (2013)Google Scholar
  63. [63]
    Martins, R., Manquinho, V., Lynce, I.: Deterministic Parallel MaxSAT Solving. International Journal on Artificial Intelligence Tools 24(3) (2015)Google Scholar
  64. [64]
    Martins, R., Manquinho, V.M., Lynce, I.: Open-WBO: A Modular MaxSAT Solver. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 438–445. Springer (2014)Google Scholar
  65. [65]
    Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints 18(4), 478–534 (2013)Google Scholar
  66. [66]
    Morgado, A., Ignatiev, A., Marques-Silva, J.: MSCG: Robust Core-Guided MaxSAT Solving. Journal on Satisfiability, Boolean Modeling and Computation 9, 129–134 (2015)Google Scholar
  67. [67]
    Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Design Automation Conference, pp. 530–535. ACM (2001)Google Scholar
  68. [68]
    Narodytska, N., Bacchus, F.: Maximum Satisfiability Using Core-Guided MaxSAT Resolution. In: Proc. AAAI Conference on Artificial Intelligence, pp. 2717–2723. AAAI Press (2014)Google Scholar
  69. [69]
    Neves, M., Lynce, I., Manquinho, V.: DistMS: A Non-Portfolio Distributed Solver for Maximum Satisfiability. In: Proc. International Conference on Tools with Artificial Intelligence. IEEE Computer Society Press (2016)Google Scholar
  70. [70]
    Neves, M., Martins, R., Janota, M., Lynce, I., Manquinho, V.M.: Exploiting resolution-based representations for MaxSAT solving. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 272–286. Springer (2015)Google Scholar
  71. [71]
    Ogawa, T., Liu, Y., Hasegawa, R., Koshimura, M., Fujita, H.: Modulo Based CNF Encoding of Cardinality Constraints and Its Application to MaxSAT Solvers. In: Proc. International Conference on Tools with Artificial Intelligence, pp. 9–17. IEEE Computer Society (2013)Google Scholar
  72. [72]
    Papadimitriou, C.M.: Computational complexity. Addison-Wesley, Reading, Massachusetts (1994)Google Scholar
  73. [73]
    Plaza, S., Kountanis, I., Andraus, Z., Bertacco, V., Mudge, T.: Advances and Insights into Parallel SAT Solving. In: Internacional Workshop on Logic & Synthesis, pp. 188–194. Conference Proceedings (2006)Google Scholar
  74. [74]
    Prestwich, S.: Variable Dependency in Local Search: Prevention is Better than Cure. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 107–120. Springer (2007)Google Scholar
  75. [75]
    Saikko, P., Berg, J., Järvisalo, M.: LMHS: A SAT-IP Hybrid MaxSAT Solver. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 539–546. Springer (2016)Google Scholar
  76. [76]
    Schubert, T., Lewis, M., Becker, B.: PaMira - A Parallel SAT Solver with Knowledge Sharing. In: Workshop on Microprocessor Test and Verification, pp. 29–36. Conference Proceedings (2005)Google Scholar
  77. [77]
    Schubert, T., Lewis, M., Becker, B.: PaMiraXT: Parallel SAT Solving with Threads and Message Passing. Journal on Satisfiability, Boolean Modeling and Computation 6, 203–222 (2009)Google Scholar
  78. [78]
    Singer, D., Monnet, A.: JaCk-SAT: A New Parallel Scheme to Solve the Satisfiability Problem (SAT) Based on Join-and-Check. In: Proc. Parallel Processing and Applied Mathematics, pp. 249–258. Springer (2008)Google Scholar
  79. [79]
    Sinz, C.: Towards an Optimal CNF Encoding of Boolean Cardinality Constraints. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 827–831. Springer (2005)Google Scholar
  80. [80]
    Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: A Cross-Community Infrastructure for Logic Solving. In: Proc. International Joint Conference on Automated Reasoning, pp. 367–373. Springer (2014)Google Scholar
  81. [81]
    Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters 68(2), 63–69 (1998)Google Scholar
  82. [82]
    Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: a Distributed Propositional Prover and Its Application to Quasigroup Problems. Journal of Symbolic Computation 21, 543–560 (1996)Google Scholar
  83. [83]
    Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient Conflict Driven Learning in Boolean Satisfiability Solver. In: Proc. International Conference on Computer-Aided Design, pp. 279–285. IEEE Computer Society Press (2001)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.INESC-ID / Instituto Superior TécnicoUniversidade de LisboaLisboaPortugal
  2. 2.University of Texas at AustinAustinUSA

Personalised recommendations