Regular Intersection Emptiness of Graph Problems: Finding a Needle in a Haystack of Graphs with the Help of Automata

TL;DR

This paper develops decision procedures for the intersection emptiness problem of graph problems with automata, enabling automated verification of graph properties through formal language techniques.

Contribution

It introduces general criteria and techniques connecting automata theory with graph problem encodings to decide intersection emptiness for various graph problems.

Findings

Applicable to Vertex Cover and Independent Set problems

Extends to subgraph, edit, and coloring problems

Provides decision procedures based on regular graph encodings

Abstract

The Int_reg-problem of a combinatorial problem P asks, given a nondeterministic automaton M as input, whether the language L(M) accepted by M contains any positive instance of the problem P. We consider the Int_reg-problem for a number of different graph problems and give general criteria that give decision procedures for these Int_reg-problems. To achieve this goal, we consider a natural graph encoding so that the language of all graph encodings is regular. Then, we draw the connection between classical pumping- and interchange-arguments from the field of formal language theory with the graph operations induced on the encoded graph. Our techniques apply among others to the Int_reg-problem of well-known graph problems like Vertex Cover and Independent Set, as well as to subgraph problems, graph-edit problems and graph-partitioning problems, including coloring problems.