SATソルバーを用いた最小無矛盾DFAの生成

概要

論文の詳細を見る
The purpose of this study is to develop efficient methods for the minimum-consistent DFA (deterministic finite state automaton) problem. The graph-coloring based SAT (satisfiability) approach proposed by Heule is a state of the art method for this problem. It specially achieves high performance computing in dense problems such as in a popular benchmark problem where rich information about labels is included. In contrast, to solve sparse problems is a challenge for the minimum-consistent DFA problem. To solve sparse problems, we propose three approaches to the SAT formulation: a) the binary color representation, b) the dynamic symmetry breaking and c) the hyper-graph coloring constraint. We organized an experiment using the existing benchmark problems and sparse problems made from them. We observed that our symmetry breaking constraints made the speed up the running time of SAT solver. In addition with this, our other proposed methods were showing the possibility to improve the performance. Then we simulated the perfomance of our methods under the condition that we executed the several program set-ups in parallel. Compared with the previous research results, we finally could reduce the average relative time by 66.5% and the total relative time by 7.6% for sparse problems and by 79.7% and 38.5% for dense problems, respectively. These results showed that our proposed methods were effective for difficult problems.