Given a Boolean formula in Conjunctive Normal Form (CNF) $\phi=S \cup H$, the MaxSAT (Maximum Satisfiability) problem asks for an assignment that satisfies the maximum number of clauses in $\phi$. Due to the good performance of current MaxSAT solvers, many real-life optimization problems such as scheduling can be solved efficiently by encoding them into MaxSAT. In this survey, we discuss the computational complexity of MaxSAT in detail in addition to major results on the classical and parameterized complexities of the problem.

Given a Boolean formula in Conjunctive Normal Form (CNF) $\phi=S \cup H$, the MaxSAT (Maximum Satisfiability) problem asks for an assignment that satisfies the maximum number of clauses in $\phi$. Due to the good performance of current MaxSAT solvers, many real-life optimization problems such as scheduling can be solved efficiently by encoding them into MaxSAT. In this survey, we discuss the computational complexity of MaxSAT in detail in addition to major results on the classical and parameterized complexities of the problem.