[2I4-OS-9a] AIと制約プログラミング

[2I4-OS-9a-03] A SAT-based Method for Solving the Maximum Independent Set Problem

〇Takane Ohmori¹, Takehide Soh¹, Naoyuki Tamura¹ (1. Kobe University)

Keywords:Maximum Independent Set Problem, Satisfiability Testing Problem, Constraint Satisfaction Problem, SAT Solver

An independent set of a given undirected graph is a subset of the vertices that does not include adjacent vertices.
The maximum independent set problem is the problem of finding the independent set with the largest number of
vertices. It is used to solve scheduling problems, design DNA sequences, etc. In this paper, we propose a method for
solving the maximum independent set problem using a SAT solver. Specifically, we propose two constraint models:
a basic constraint model and an improved constraint model using a clique cover. We also propose an algorithm
for solving the maximum independent set problem using incremental SAT method, which speeds up the process by
reusing learnt clauses obtained in the search process. As an evaluation of the proposed method, we compared it
with existing methods for the maximum independent set problem and confirmed the effectiveness of the proposed
method.