Abstract
We de?ne solving techniques for the Minimum Satis?ability Problem (MinSAT), propose an ef?cient branch-and-bound algorithm to solve the Weighted Partial MinSAT problem, and report on an empirical evaluation of the algorithm on Min-3SAT, MaxClique, and combinatorial auction problems. Techniques solving MinSAT are substantially different from those for the Maximum Satis?ability Problem (MaxSAT). Our results provide empirical evidence that solving combinatorial optimization problems by reducing them to MinSAT may be substantially faster than reducing them to MaxSAT, and even competitive with speci?c algorithms. We also use MinSAT to study an interesting correlation between the minimum number and the maximum number of satis?ed clauses of a SAT instance.