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.
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 p
s 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