Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Iterative and core-guided MaxSAT solving: A survey and assessment

  • Survey
  • Published:
Constraints Aims and scope Submit manuscript

Abstract

Maximum Satisfiability (MaxSAT) is an optimization version of SAT, and many real world applications can be naturally encoded as such. Solving MaxSAT is an important problem from both a theoretical and a practical point of view. In recent years, there has been considerable interest in developing efficient algorithms and several families of algorithms have been proposed. This paper overviews recent approaches to handle MaxSAT and presents a survey of MaxSAT algorithms based on iteratively calling a SAT solver which are particularly effective to solve problems arising in industrial settings. First, classic algorithms based on iteratively calling a SAT solver and updating a bound are overviewed. Such algorithms are referred to as iterative MaxSAT algorithms. Then, more sophisticated algorithms that additionally take advantage of unsatisfiable cores are described, which are referred to as core-guided MaxSAT algorithms. Core-guided MaxSAT algorithms use the information provided by unsatisfiable cores to relax clauses on demand and to create simpler constraints. Finally, a comprehensive empirical study on non-random benchmarks is conducted, including not only the surveyed algorithms, but also other state-of-the-art MaxSAT solvers. The results indicate that (i) core-guided MaxSAT algorithms in general abort in less instances than classic solvers based on iteratively calling a SAT solver and that (ii) core-guided MaxSAT algorithms are fairly competitive compared to other approaches.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Aksoy, L., daCosta, E.A.C., Flores, P.F., Monteiro, J. (2008). Exact and approximate algorithms for the optimization of area and delay in multiple constant multiplications. IEEE Transactions on CAD of Integrated Circuits and Systems on CAD, 27(6), 1013–1026.

    Article  Google Scholar 

  2. Aloul, F., Ramani, A., Markov, I., Sakallah, K. (2002). PBS: A backtrack search pseudo-Boolean solver. In Symposium on theory and applications of satisfiability testing (pp. 346–353).

  3. Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A. (2002). Generic ILP versus specialized 0-1 ILP: An update. In International conference on computer-aided design (pp. 450–457).

  4. Andres, B., Kaufmann, B., Matheis, O., Schaub, T. (2012). Unsatisfiability-based optimization in clasp. In International conference on logic programming (Technical communications) (pp. 211–221).

  5. Anjos, M.F. (2006). Semidefinite optimization approaches for satisfiability and maximum-satisfiability problems. Journal on Satisfiability, Boolean Modeling and Computation, 1(1), 1–47.

    MathSciNet  MATH  Google Scholar 

  6. Ansótegui, C., Bonet, M.L., Gabàs, J., Levy, J. (2012). Improving SAT-based weighted MaxSAT solvers. In International conference on principles and practice of constraint programming (pp. 86–101).

  7. Ansótegui, C., Bonet, M.L., Levy, J. (2009). On solving MaxSAT through SAT. In International conference of the Catalan Association for artificial intelligence (pp. 284–292).

  8. Ansótegui, C., Bonet, M.L., Levy, J. (2009). Solving (weighted) partial MaxSAT through satisfiability testing. In International conference on theory and applications of satisfiability testing (pp. 427–440).

  9. Ansótegui, C., Bonet, M.L., Levy, J. (2010). A new algorithm for weighted partial MaxSAT. In AAAI conference on artificial intelligence (pp. 3–8).

  10. Ansótegui, C., Bonet, M.L., Levy, J. (2013). SAT-based MaxSAT algorithms. In Artificial inteligence journal (Vol. 196, pp. 77–105).

  11. Ansótegui, C., & Manyà, F. (2004). Mapping problems with finite-domain variables into problems with Boolean variables. In International conference on theory and applications of satisfiability testing (pp. 111–119).

  12. Ardagna, C.A., diVimercati, S.D.C., Foresti, S., Paraboschi, S., Samarati, P. (2010). Minimizing disclosure of private information in credential-based interactions: A graph-based approach. In International conference on social computing/international conference on privacy, security, risk and trust (pp. 743–750).

  13. Argelich, J., Berre, D.L., Lynce, I., Marques-Silva, J., Rapicault, P. (2010). Solving linux upgradeability problems using Boolean optimization. In International workshop on logics for component configuration (pp. 11–22).

  14. Argelich, J., Li, C.M., Manya, F., Planes, J. (2011). Experimenting with the instances of the MaxSAT Evaluation. In International conference of the catalan association for artificial intelligence (pp. 360–361).

  15. Argelich, J., & Lynce, I. (2008). CNF instances from the software package installation problem. In RCRA international workshop on “Experimental Evaluation of Algorithms for solving problems with combinatorial explosion”.

  16. Argelich, J., Lynce, I., Marques-Silva, J. (2009). On solving Boolean multilevel optimization problems. In International joint conference on artificial intelligence (pp. 393–398).

  17. Asín, R., & Nieuwenhuis, R. (2010). Curriculum-based course timetabling with SAT and MaxSAT. In International conference on the practice and theory of automated timetabling (pp. 42–56).

  18. Asín, R., & Nieuwenhuis, R. (2012). Curriculum-based course timetabling with SAT and MaxSAT. Annals of Operations Research, 1–21.

  19. Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E. (2011). Cardinality networks: a theoretical and empirical study. Constraints, 16(2), 195–221.

    Article  MathSciNet  MATH  Google Scholar 

  20. Bailleux, O., & Boufkhad, Y. (2003). Efficient CNF encoding of Boolean cardinality constraints. In International conference on principles and practice of constraint programming (pp. 108–122).

  21. Bansal, N., & Raman, V. (1999). Upper bounds for MaxSat: Further improved. In International symposium on algorithms and computation (pp. 247–258).

  22. Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C. (2009). Satisfiability modulo theories. In Handbook of satisfiability (pp. 825–884). IOS Press.

  23. Barth, P. (1995). A Davis-Putnam enumeration algorithm for linear pseudo-Boolean optimization. Technical Report MPI-I-95-2-003, Max Plank Institute for Computer Science.

  24. Batcher, K.E. (1968). Sorting networks and their applications. In AFIPS spring joint computing conference (pp. 307–314).

  25. Berre, D.L., & Parrain, A. (2010). The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation, 7, 59–64.

    Google Scholar 

  26. Biere, A. (2008). PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation, 2, 75–97.

    Google Scholar 

  27. Birnbaum, E., & Lozinskii, E.L. (2003). Consistent subsets of inconsistent systems: structure and behaviour. Journal of Experimental and Theoretical Artificial Intelligence, 15(1), 25–46.

    Article  MATH  Google Scholar 

  28. Bonet, M.L., Levy, J., Manyà, F. (2007). Resolution for Max-SAT. Artificial Intelligence Journal, 171(8–9), 606–618.

    Article  MATH  Google Scholar 

  29. Borchers, B., & Furman, J. (1999). A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems. Journal of Combinatorial Optimization, 2, 299–306.

    Article  MathSciNet  MATH  Google Scholar 

  30. Brihaye, T., Bruyère, V., Doyen, L., Ducobu, M., Raskin, J.-F. (2011). Antichain-based QBF solving. In International symposium on automated technology for verification and analysis (pp. 183–197).

  31. Cha, B., Iwama, K., Kambayashi, Y., Miyazaki, S. (1997). Local search algorithms for partial MaxSAT. In AAAI conference on artificial intelligence/IAAI innovative applications of artificial intelligence conference (pp. 263–268).

  32. Chai, D., & Kuehlmann, A. (2003). A fast pseudo-Boolean constraint solver. In Design automation conference (pp. 830–835).

  33. Chen, Y., Safarpour, S., Marques-Silva, J., Veneris, A.G. (2010). Automated design debugging with maximum satisfiability. IEEE Transactions on CAD of Integrated Circuits and Systems, 29(11), 1804–1817.

    Article  Google Scholar 

  34. Chen, Y., Safarpour, S., Veneris, A., Marques-Silva, J. (2009). Spatial and temporal design debug using partial MaxSAT. In IEEE great lakes symposium on VLSI.

  35. Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R., Stenico, C. (2010). Satisfiability modulo the theory of costs: Foundations and applications. In International conference tools and algorithms for the construction and analysis of systems (pp. 99–113).

  36. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R. (2013). A modular approach to MaxSAT modulo theories. In International conference on theory and applications of satisfiability testing (pp. 150–165).

  37. Codish, M., Lagoon, V., Stuckey, P.J. (2008). Logic programming with satisfiability. Journal of Theory and Practice of Logic Programming, 8(1), 121–128.

    MATH  Google Scholar 

  38. Cooper, M.C., Cussat-Blanc, S., deRoquemaurel, M., Régnier, P. (2006). Soft arc consistency applied to optimal planning. In International conference on principles and practice of constraint programming (pp. 680–684).

  39. Cooper, M.C., deGivry, S., Sanchez, M., Schiex, T., Zytnicki, M., Werner, T. (2010). Soft arc consistency revisited. Artificial Intelligence Journal, 174(7–8), 449–478.

    Article  MathSciNet  MATH  Google Scholar 

  40. Davies, J., & Bacchus, F. (2011). Solving MaxSAT by solving a sequence of simpler SAT instances. In International conference on principles and practice of constraint programming (pp. 225–239).

  41. Davies, J., Cho, J., Bacchus, F. (2010). Using learnt clauses in MaxSAT. In International conference on principles and practice of constraint programming (pp. 176–190).

  42. deGivry, S., Larrosa, J., Meseguer, P., Schiex, T. (2003). Solving Max-SAT as weighted CSP. In International conference on principles and practice of constraint programming (pp. 363–376).

  43. deMoura, L.M., & Bjørner, N. (2008). Z3: An efficient SMT solver. In International conference tools and algorithms for the construction and analysis of systems (pp. 337–340).

  44. Eén, N., & Sörensson, N. (2003). An extensible SAT-solver. In International conference on theory and applications of satisfiability testing (pp. 502–518).

  45. Een, N., & Sörensson, N. (2006). Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2, 1–26.

    MATH  Google Scholar 

  46. Feldman, A., Provan, G., deKleer, J., Robert, S., van Gemund, A. (2010). Solving model-based diagnosis problems with MaxSAT solvers and vice versa. In International workshop on the principles of diagnosis.

  47. Fu, Z., & Malik, S. (2006). On solving the partial MAX-SAT problem. In International conference on theory and applications of satisfiability testing (pp. 252–265).

  48. Gebser, M., Kaufmann, B., Schaub, T. (2009). The conflict-driven answer set solver clasp: Progress report. In International conference on logic programming and nonmonotonic reasoning (pp. 509–514).

  49. Gent, I.P., & Nightingale, P. (2004). A new encoding of alldifferent into SAT. In International workshop on modelling and reformulating constraint satisfaction problems (pp. 95–110).

  50. Giunchiglia, E., Lierler, Y., Maratea, M. (2006). Answer set programming based on propositional satisfiability. Journal of Automated Reasoning, 36(4), 345–377.

    Article  MathSciNet  MATH  Google Scholar 

  51. Giunchiglia, E., & Maratea, M. (2006). Optsat: A tool for solving SAT related optimization problems. In European conference on logics in artificial intelligence (JELIA) (pp. 485–489).

  52. Giunchiglia, E., & Maratea, M. (2006). Solving optimization problems with DLL. In European conference on artificial intelligence (pp. 377–381).

  53. Giunchiglia, E., & Maratea, M. (2007). Planning as satisfiability with preferences. In AAAI conference on artificial intelligence (pp. 987–992).

  54. Gomes, C.P., van Hoeve, W.J., Leahu, L. (2006). The power of semidefinite programming relaxations for Max-SAT. In International conference integration of AI and OR techniques in constraint programming for combinatorial optimization problems (pp. 104–118).

  55. Gottlob, G. (1995). NP trees and Carnap’s modal logic. Journal of ACM, 42(2), 421–457.

    Article  MathSciNet  MATH  Google Scholar 

  56. Graca, A., Lynce, I., Marques-Silva, J., Oliveira, A. (2010). Efficient and accurate haplotype inference by combining parsimony and pedigree information. In International conference algebraic and numeric biology (pp. 38–56).

  57. Graca, A., Marques-Silva, J., Lynce, I., Oliveira, A. (2011). Haplotype inference with pseudo-Boolean optimization. Annals of Operations Research, 184(1), 137–162.

    Article  MathSciNet  MATH  Google Scholar 

  58. Guerra, J., & Lynce, I. (2012). Reasoning over biological networks using maximum satisfiability. In International conference on principles and practice of constraint programming (pp. 941–956).

  59. Hachtel, G.D., & Somenzi, F. (1996). Logic synthesis and verification algorithms. Kluwer.

  60. Heras, F., Larrosa, J., deGivry, S., Schiex, T. (2008). 2006 and 2007 Max-SAT evaluations: contributed instances. Journal on Satisfiability, Boolean Modeling and Computation, 4(2–4), 239–250.

    MATH  Google Scholar 

  61. Heras, F., Larrosa, J., Oliveras, A. (2008). MiniMaxSat: an efficient weighted Max-SAT solver. Journal of Artificial Intelligence Research, 31, 1–32.

    MathSciNet  MATH  Google Scholar 

  62. Heras, F., & Marques-Silva, J. (2011). Read-once resolution for unsatisfiability-based Max-SAT algorithms. In International joint conference on artificial intelligence (pp. 572–577).

  63. Heras, F., Morgado, A., Marques-Silva, J. (2011). Core-guided binary search for maximum satisfiability. In AAAI conference on artificial intelligence.

  64. Hoos, H., & Stützle, T. (2005). Stochastic local search: Foundations and applications. Morgan Kaufmann.

  65. Hoos, H.H. (2002). An adaptive noise mechanism for WalkSAT. In AAAI conference on artificial intelligence/IAAI innovative applications of artificial intelligence conference (pp. 655–660).

  66. Jose, M., & Majumdar, R. (2011). Bug-assist: Assisting fault localization in ANSI-C programs. In International conference on computer aided verification (pp. 504–509).

  67. Jose, M., & Majumdar, R. (2011). Cause clue clauses: Error localization using maximum satisfiability. In ACM SIGPLAN conference on programming language design and implementation (pp. 437–446).

  68. Juma, F., Hsu, E.I., McIlraith, S.A. (2012). Preference-based planning via MaxSAT. In Canadian conference on AI (pp. 109–120).

  69. Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R. (2012). QMaxSAT: a partial Max-SAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 8, 95–100.

    MathSciNet  Google Scholar 

  70. Kuegel, A. (2010). Improved exact solver for the weighted MAX-SAT problem. In Pragmatics of SAT.

  71. Larrosa, J., & Heras, F. (2005). Resolution in Max-SAT and its relation to local consistency in weighted CSPs. In International joint conference on artificial intelligence (pp. 193–198).

  72. Larrosa, J., Heras, F., deGivry, S. (2008). A logical approach to efficient Max-SAT solving. Artificial Inteligence Journal, 172(2–3), 204–233.

    Article  MathSciNet  MATH  Google Scholar 

  73. Larrosa, J., & Schiex, T. (2004). Solving weighted CSP by maintaining arc consistency. Artificial Inteligence Journal, 159(1–2), 1–26.

    Article  MathSciNet  MATH  Google Scholar 

  74. Li, C.M., & Manyà, F. (2009). MaxSAT, hard and soft constraints. In Handbook of satisfiability (pp. 613–632). IOS Press.

  75. Li, C.M., Manyà, F., Planes, J. (2005). Exploiting unit propagation to compute lower bounds in branch and bound Max-SAT solvers. In International conference on principles and practice of constraint programming (pp. 403–414).

  76. Li, C.M., Manyà, F., Planes, J. (2007). New inference rules for Max-SAT. Journal of Artificial Intelligence Research, 30, 321–359.

    MathSciNet  Google Scholar 

  77. Liffiton, M.H., Sakallah, K.A. (2005). On finding all minimally unsatisfiable subformulas. In International conference on theory and applications of satisfiability testing (pp. 173–186).

  78. Liffiton, M.H., & Sakallah, K.A. (2008). Algorithms for computing minimal unsatisfiable subsets of constraints. Journal Automated Reasoning, 40(1), 1–33.

    Article  MathSciNet  MATH  Google Scholar 

  79. Lin, H., Su, K., Li, C.M. (2008). Within-problem learning for efficient lower bound computation in Max-SAT solving. In AAAI conference on artificial intelligence (pp. 351–356).

  80. Mancinelli, F., Boender, J., diCosmo, R., Vouillon, J., Durak, B., Leroy, X., Treinen, R. (2006). Managing the complexity of large free and open source package-based software distributions. In International conference on automated software engineering (pp. 199–208).

  81. Mangassarian, H., Veneris, A.G., Safarpour, S., Najm, F.N., Abadir, M.S. (2007). Maximum circuit activity estimation using pseudo-Boolean satisfiability. In Conference on design, automation and test in Europe (pp. 1538–1543).

  82. Manquinho, V., Marques-Silva, J., Planes, J. (2009). Algorithms for weighted Boolean optimization. In International conference on theory and applications of satisfiability testing (pp. 495–508).

  83. Manquinho, V., Martins, R., Lynce, I. (2010). Improving unsatisfiability-based algorithms for Boolean optimization. In International conference on theory and applications of satisfiability testing (pp. 181–193).

  84. Marques-Silva, J., Argelich, J., Graça, A., Lynce, I. (2011). Boolean lexicographic optimization: Algorithms & applications. Annals of Mathematics and Artificial Intelligence, 62(3–4), 317–343.

    Article  MathSciNet  MATH  Google Scholar 

  85. Marques-Silva, J., & Manquinho, V. (2008). Towards more effective unsatisfiability-based maximum satisfiability algorithms. In International conference on theory and applications of satisfiability testing (pp. 225–230).

  86. Marques-Silva, J., & Planes, J. (2007). On using unsatisfiability for solving maximum satisfiability. Computing Research Repository. arXiv: abs/0712.0097.

  87. Marques-Silva, J., Planes, J. (2008). Algorithms for maximum satisfiability using unsatisfiable cores. In Conference on design, automation and testing in Europe (pp. 408–413).

  88. Marques-Silva, J., & Sakallah, K.A. (1996). GRASP—a new search algorithm for satisfiability. In International conference on computer-aided design (pp. 220–227).

  89. Martins, R., Manquinho, V., Lynce, I. (2012). On partitioning for maximum satisfiability. In European conference on artificial intelligence (pp. 913–914).

  90. Martins, R., Manquinho, V.M., Lynce, I. (2013). Community-based partitioning for MaxSAT solving. In International conference on theory and applications of satisfiability testing (pp. 182–191).

  91. Morgado, A., Heras, F., Marques-Silva, J. (2011). The MSUnCore MaxSAT solver. In Pragmatics of SAT.

  92. Morgado, A., Heras, F., Marques-Silva, J. (2012). Improvements to core-guided binary search for MaxSAT. In Theory and applications of satisfiability testing (pp. 284–297).

  93. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S. (2001). Chaff: Engineering an efficient SAT solver. In Design automation conference (pp. 530–535).

  94. Neveu, B., Trombettoni, G., Glover, F. (2004). ID Walk: A candidate list strategy with a simple diversification device. In International conference on principles and practice of constraint programming (pp. 423–437).

  95. Niedermeier, R., Rossmanith, P. (2000). New upper bounds for maximum satisfiability. Journal of Algorithms, 36(1), 63–88.

    Article  MathSciNet  MATH  Google Scholar 

  96. Nieuwenhuis, R., & Oliveras, A. (2006). On SAT modulo theories and optimization problems. In International conference on theory and applications of satisfiability testing (pp. 156–169).

  97. Nieuwenhuis, R., Oliveras, A., Tinelli, C. (2006). Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). Journal of ACM, 53(6), 937–977.

    Article  MathSciNet  Google Scholar 

  98. Oikarinen, E., Järvisalo, M. (2009). Max-ASP: Maximum satisfiability of answer set programs. In International conference on logic programming and nonmonotonic reasoning (pp. 236–249).

  99. Palubeckis, G. (2009). A new bounding procedure and an improved exact algorithm for the MAX-2-SAT problem. Applied Mathematics and Computation, 215(3), 1106–1117.

    Article  MathSciNet  MATH  Google Scholar 

  100. Papadimitriou, C. (1994). Computational complexity. USA: Addison-Wesley.

    MATH  Google Scholar 

  101. Papadimitriou, C., & Zachos, S. (1983). Two remarks on the power of counting. Theoretical Computer Science, 269–276.

  102. Park, J.D. (2002). Using weighted MAX-SAT engines to solve MPE. In AAAI conference on artificial intelligence (pp. 682–687).

  103. Pipatsrisawat, K., Palyan, A., Chavira, M., Choi, A., Darwiche, A. (2008). Solving weighted Max-SAT problems in a reduced search space: a performance analysis. Journal on Satisfiability Boolean Modeling and Computation, 4, 191–217.

    MATH  Google Scholar 

  104. Prestwich, S. (2009). CNF encodings. In Handbook of satisfiability (pp. 75–98). IOS Press.

  105. Prestwich, S.D. (2007). Variable dependency in local search: Prevention is better than cure. In International conference on theory and applications of satisfiability testing (pp. 107–120).

  106. Ramírez, M., & Geffner, H. (2007). Structural relaxations by variable renaming and their compilation for solving MinCostSAT. In International conference on principles and practice of constraint programming (pp. 605–619).

  107. Reiter, R. (1987). A theory of diagnosis from first principles. Artificial Inteligence Journal, 32(1), 57–95.

    Article  MathSciNet  MATH  Google Scholar 

  108. Robinson, N., Gretton, C., Pham, D.N., Sattar, A. (2010). Partial weighted MaxSAT for optimal planning. In Pacific rim international conference on artificial intelligence (pp. 231–243).

  109. Rosa, E.D., Giunchiglia, E., Maratea, M. (2010). Solving satisfiability problems with preferences. Constraints, 15(4), 485–515.

    Article  MathSciNet  MATH  Google Scholar 

  110. Roussel, O., & Manquinho, V. (2009). Pseudo-Boolean and cardinality constraints. In Handbook of satisfiability (pp. 695–734). IOS Press.

  111. Safarpour, S., Mangassarian, H., Veneris, A., Liffiton, M.H., Sakallah, K.A. (2007). Improved design debugging using maximum satisfiability. In Formal methods in computer-aided design.

  112. Sandholm, T. (1999). An algorithm for optimal winner determination in combinatorial auctions. In International joint conference on artificial intelligence (pp. 542–547).

  113. Sebastiani, R. (2007). Lazy satisfiability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation, 3, 141–224.

    MathSciNet  MATH  Google Scholar 

  114. Sebastiani, R., & Tomasi, S. (2012). Optimization in SMT with LA(Q) cost functions. In International joint conference in automated reasoning (pp. 484–498).

  115. Selman, B., Kautz, H.A., Cohen, B. (1994). Noise strategies for improving local search. In AAAI conference on artificial intelligence (pp. 337–343).

  116. Selman, B., Levesque, H.J., Mitchell, D.G. (1992). A new method for solving hard satisfiability problems. In AAAI conference on artificial intelligence (pp. 440–446).

  117. Sheini, H., & Sakallah, K. (2006). Pueblo: a hybrid pseudo-Boolean SAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 2(3–4), 165–189.

    Google Scholar 

  118. Shen, H., & Zhang, H. (2005). Improving exact algorithms for MAX-2-SAT. Annals of Mathematics and Artificial Intelligence, 44(4), 419–436.

    Article  MathSciNet  MATH  Google Scholar 

  119. Sinz, C. (2005). Towards an optimal CNF encoding of Boolean cardinality constraints. In International conference on principles and practice of constraint programming (pp. 827–831).

  120. Strickland, D., Barnes, E., Sokol, J. (2005). Optimal protein structure alignment using maximum cliques. Operations Research, 53(3), 389–402.

    Article  MathSciNet  MATH  Google Scholar 

  121. Teresa Alsinet, J.P., Manyà, F. (2004). A Max-SAT solver with lazy data structures. In Ibero-American conference on AI (IBERAMIA) (pp. 334–342).

  122. Tompkins, D.A.D., & Hoos, H.H. (2004). UBCSAT: An implementation and experimentation environment for SLS algorithms for SAT & Max-SAT. In International conference on theory and applications of satisfiability testing (pp. 37–46).

  123. Tucker, C., Shuffelton, D., Jhala, R., Lerner, S. (2007). OPIUM: Optimal package install/uninstall manager. In International conference on software engineering (pp. 178–188).

  124. Vasquez, M., & Hao, J. (2001). A logic-constrained knapsack formulation and a tabu algorithm for the daily photograph scheduling of an earth observation satellite. Journal of Computational Optimization and Applications, 20(2), 137–157.

    Article  MathSciNet  MATH  Google Scholar 

  125. Warners, J.P. (1998). A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 68(2), 63–69.

    Article  MathSciNet  Google Scholar 

  126. Xing, Z., & Zhang, W. (2005). MaxSolver: an efficient exact algorithm for (weighted) maximum satisfiability. Artificial Inteligence Journal, 164(1–2), 47–80.

    Article  MathSciNet  MATH  Google Scholar 

  127. Xu, H., Rutenbar, R., Sakallah, K. (2002). sub-SAT: A formulation for relaxed boolean satisfiability with applications in routing. In International symposium on physical design (pp. 182–187).

  128. Zhang, L., & Malik, S. (2003). Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In Conference on design, automation and testing in Europe (pp. 10880–10885).

  129. Zhang, L., & Bacchus, F. (2012). MaxSAT heuristics for cost optimal planning. In AAAI conference on artificial intelligence (pp. 1846–1852).

  130. Zhu, C.S., Weissenbacher, G., Malik, S. (2011). Post-silicon fault localisation using maximum satisfiability and backbones. In Formal methods in computer-aided design (pp. 63–66).

Download references

Author information

Authors and Affiliations

  1. CSI/CASL, University College Dublin, Dublin, Ireland

    Antonio Morgado, Federico Heras & Joao Marques-Silva

  2. Illinois Wesleyan University, Bloomington, IL, USA

    Mark Liffiton

  3. Universitat de Lleida, Lleida, Spain

    Jordi Planes

  4. IST/INESC-D, Universidade Tecnica de Lisboa, Lisboa, Portugal

    Joao Marques-Silva

Authors
  1. Antonio Morgado
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Federico Heras
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mark Liffiton
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jordi Planes
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Joao Marques-Silva
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Antonio Morgado.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Morgado, A., Heras, F., Liffiton, M. et al. Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints 18, 478–534 (2013). https://doi.org/10.1007/s10601-013-9146-2

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10601-013-9146-2

Keywords

Search

Navigation