Minimum Satisfiability and its Applications
Chumin Li, Zhu Zhu, Felip Manya and Laurent Simon
We define original solving techniques for the Minimum Satisfiability Problem (MinSAT), describe an efficient branch-and-bound algorithm for solving the Weighted Partial MinSAT problem, and report on an empirical evaluation. Techniques solving MinSAT are substantially different from those for the Maximum Satisfiability Problem (MaxSAT). For example, while unit propagation is essential in solving MaxSAT, it is restricted to hard clauses in our approach. Our results provide empirical evidence that solving combinatorial optimization problems by reducing them to MinSAT can be substantially faster than reducing them to MaxSAT, and even competitive with specific algorithms. MinSAT also allows us to study an interesting correlation between the minimum number and the maximum number of satisfied clauses of a SAT instance, suggesting a new direction of research to characterize the satisfiability of the instance.