Search code examples
satsatisfiability

Why is MAX-SAT a generalisation of the SAT problem?


According to Wikipedia, the maximum satisfiability problem (MAX-SAT) is the problem of determining the maximum number of clauses, of a given Boolean formula in conjunctive normal form, that can be made true by an assignment of truth values to the variables of the formula. It is a generalisation of the Boolean satisfiability problem, which asks whether there exists a truth assignment that makes all clauses true.

I do not understand the 2nd sentence on how MAX-SAT is a generalisation of SAT. According to Wikipedia, SAT asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE.

The reason why I am asking this is because of the paper 'Semidefinite Optimization Approaches for Satisfiability and Maximum-Satisfiability Problems', where I would like to try Semidefinite optimisation techniques to solve some SAT problems I have at hand.


Solution

  • Imagine turning each of your clauses to implications, by adding p -> q where p is a fresh variable for each clause q you have in your original problem. Then, a satisfying instance to this modified problem is a solution to MAXSAT problem of the original, when you pick those clauses where the solver assigned true to the corresponding p. This gives you a maxsat solver, albeit a crappy one.

    Now imagine you have a system that makes sure it makes as many of those p's true as possible. That combination now gives you a maxsat solver, i.e., one that can optimize the number of ps that are true. This way you get a nice maxsat solver for your original problem, i.e., you can reduce the maxsat problem to sat, provided you have something that maximizes the number of true assignment to those p's that you introduce through the translation.

    @PatrickTrentin can probably explain much better! The vZ paper (the maxsat engine associated with z3) is also a very nice and simple read on this topic: https://backend.orbit.dtu.dk/ws/portalfiles/portal/110977246/Bj_rner_Phan_Fleckenstein_Unknown_Z_An_Optimizing_SMT_Solver_1.pdf