SQUARE COLORING PLANAR GRAPHS WITH AUTOMATIC DISCHARGING

The discharging method is a powerful proof technique, especially for graph coloring problems. Its major downside is that it often requires lengthy case analyses, which are sometimes given to a computer for verification. However, it is much less common to use a computer to actively look for a discharging proof. In this paper, we use a linear programming approach to automatically look for a discharging proof. While our system is not entirely autonomous, we manage to make some progress toward Wegner's conjecture for distance -2 coloring of planar graphs by showing that 12 colors are sufficient to color at distance 2 every planar graph with maximum degree 4.