TitleMaxSAT, Hard and Soft Constraints
Publication TypeBook Chapter
Year of Publication2009
AuthorsLi CMin, Manyà F
EditorBiere A, Heule MJH, van Maaren H, Walsh T
Book TitleHandbook of Satisfiability
PublisherIOS Press
ISBN Number978-1-58603-929-5

MaxSAT solving is becoming a competitive generic approach for solving combinatorial optimization problems, partly due to the development of new solving techniques that have been recently incorporated into modern MaxSAT solvers, and to the challenge problems posed at the MaxSAT Evaluations. In this chapter we present the most relevant results on both approximate and exact MaxSAT solving, and survey in more detail the techniques that have proven to be useful in branch and bound MaxSAT and Weighted MaxSAT solvers. Among such techniques, we pay special attention to the definition of good quality lower bounds, powerful inference rules, clever variable selection heuristics and suitable data structures. Moreover, we discuss the advantages of dealing with hard and soft constraints in the Partial MaxSAT formalims, and present a summary of the MaxSAT Evaluations that have been organized so far as affiliated events of the International Conference on Theory and Applications of Satisfiability Testing.