On Reducing Maximum Independent Set to Minimum Satisfiability

ABSTRACT. Maximum Independet Set (MIS) is a well-known NP-hard graph problem, tightly related with other well known NP-hard graph problems, namely Minimum Vertex Cover (MVC) and Maximum Clique (MaxClq). This paper introduces a novel reduction of MIS into Minimum Satisfiability (MinSAT). Besides providing an alternative approach for solving MIS, the proposed reduction serves as a simpler alternative proof of the NP-hardness of MinSAT. The reduction naturally maps the vertices of a graph into clauses, without requiring the inclusion of hard clauses. Moreover, it is shown that the proposed reduction uses fewer variables and clauses than the existing alternative of mapping MIS into Maximum Satisfiability (MaxSAT). The paper develops a number of optimizations to the basic reduction, which significantly reduce the total number of variables used. The experimental evaluation considered the reductions described in the paper as well as existing state-of-the-art approaches. The results show that the proposed approaches based on MinSAT are competitive with existing approaches.