Abstract
Maximum satisfiability (MaxSAT) is an optimization version of Boolean satisfiability (SAT) that can be applied to a variety of computationally hard optimization problems at large. Constituting a declarative approach to optimization, modern state-of-the-art MaxSAT solvers allow for efficiently tackling NP-hard optimization problems arising from different applications via simple propositional encodings. MaxSAT offers an alternative to, for example, the more classical declarative optimization paradigm of integer programming (IP), especially in the many applications where the underlying problems are naturally represented with logical constraints. Focusing on practical algorithmic aspects, we give an overview of different search techniques that have been developed for MaxSAT, covering both complete and incomplete MaxSAT solving. The talk is a revised and updated version of earlier tutorials presented at ECAI 2020 and AAAI 2016.