Maximum Boolean satisfiability (max-SAT) is the optimization counterpart of Boolean satisfiability (SAT), in which a variable assignment is sought to satisfy the maximum number of clauses in a Boolean formula. A branch and bound algorithm based on the Davis–Putnam–Logemann–Loveland procedure (DPLL) is one of the most competitive exact algorithms for solving max-SAT. In this paper, we propose and investigate a number of strategies for max-SAT. The first strategy is a set of unit propagation or unit resolution rules for max-SAT. We summarize three existing unit propagation rules and propose a new one based on a nonlinear programming formulation of max-SAT. The second strategy is an effective lower bound based on linear programming (LP). We show that the LP lower bound can be made effective as the number of clauses increases. The third strategy consists of a binary-claus! e first rule and a dynamic-weighting variable ordering rule, which are motivated by a thorough analysis of two existing well-known variable orderings. Based on the analysis of these strategies, we develop an exact solver for both max-SAT and weighted max-SAT. Our experimental results on random problem instances and many instances from the max-SAT libraries show that our new solver outperforms most of the existing exact max-SAT solvers, with orders of magnitude of improvement in many cases.

References in zbMATH (referenced in 19 articles , 1 standard article )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. Morgado, Antonio; Heras, Federico; Liffiton, Mark; Planes, Jordi; Marques-Silva, Joao: Iterative and core-guided maxsat solving: a survey and assessment (2013)
  2. van Hoeve, Willem-Jan: Semidefinite programming and constraint programming (2012)
  3. Arieli, Ofer; Zamansky, Anna: A framework for reasoning under uncertainty based on non-deterministic distance semantics (2011)
  4. Ibaraki, Toshihide; Imamichi, Takashi; Koga, Yuichi; Nagamochi, Hiroshi; Nonobe, Koji; Yagiura, Mutsunori: Efficient branch-and-bound algorithms for weighted MAX-2-SAT (2011)
  5. Larrosa, Javier; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric: A framework for certified Boolean branch-and-bound optimization (2011)
  6. Mengshoel, Ole J.; Roth, Dan; Wilkins, David C.: Portfolios in stochastic local search: efficiently computing most probable explanations in Bayesian networks (2011)
  7. Crama, Yves (ed.); Hammer, Peter L. (ed.): Boolean models and methods in mathematics, computer science, and engineering (2010)
  8. Di Rosa, Emanuele; Giunchiglia, Enrico; Maratea, Marco: Solving satisfiability problems with preferences (2010)
  9. Larrosa, Javier; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric: Branch and bound for Boolean optimization and the generation of optimality certificates (2009)
  10. Palubeckis, Gintaras: A new bounding procedure and an improved exact algorithm for the Max-2-SAT problem (2009)
  11. Boughaci, Dalila; Benhamou, Belaïd; Drias, Habiba: Scatter search and genetic algorithms for MAX-SAT problems (2008)
  12. Heras, F.; Larrosa, J.; Oliveras, A.: Minimaxsat: an efficient weighted Max-SAT solver (2008)
  13. Larrosa, Javier; Heras, Federico; de Givry, Simon: A logical approach to efficient Max-SAT solving (2008)
  14. Eiter, Thomas; Erdem, Esra; Fink, Michael; Senko, Ján: Comparing action descriptions based on semantic preferences (2007)
  15. Argelich, Josep; Manyà, Felip: Exact Max-SAT solvers for over-constrained problems (2006)
  16. Argelich, Josep; Manyà, Felip: Exact Max-SAT solvers for over-constrained problems (2006)
  17. Gomes, Carla P.; van Hoeve, Willem-Jan; Leahu, Lucian: The power of semidefinite programming relaxations for MAX-SAT (2006)
  18. Nieuwenhuis, Robert; Oliveras, Albert: On SAT modulo theories and optimization problems (2006)
  19. Xing, Zhao; Zhang, Weixiong: MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability (2005)