Derrick Stolee - Iowa State University - Research Browser

ADAGE: Automated Discharging Arguments using GEneration
The ADAGE Framework

The ADAGE Framework is a general-purpose framework for automating discharging arguments. Since an adage is a short phrase that conveys a deeper meaning, so does an adage proof provide a very short description of a discharging argument such that a computer can perform the long case analysis to verify the argument. This framework is planned to expand to several domains, but currently is only implemented for density problems on grids.

The framework has four distinct steps.

  1. Define notions of forbidden and/or reducible configurations.
  2. Define a charge function and design discharging rules. (But do not assign value!)
  3. Construct all possible arrangements of discharging rules simultaneously acting on an object, and create a linear constraint for each.
  4. Solve a linear program that assigns value to the discharging rules such that the discharging assertions are guaranteed.

This way of constructing a linear program using combinatorial generation and solving it to find "the best proof using these structures" is very similar to the use of semidefinite programming in Razborov's flag algebras.

ADAGE on Grids

If $G$ is a plane grid, then let $X \subset V(G)$ be a set of vertices satisfying some property. We aim to define a lower bound on the density of $X$, defined as

$\delta(X) = \limsup_{r\to\infty} \frac{|B_r(v)\cap X|}{|B_r(v)|}.$
This density can be bounded below by the use of discharging arguments.

The ADAGE framework was implemented for density problems in grids, especially attacking identifying codes and variations on identifying codes. The main theorem is the following bound that improves on all previous human-written proofs.

Theorem. The minimum density of an identifying code in the hexagonal grid is at least $\frac{23}{55} = 0.4\overline{18}$.

This does not yet match the current-best upper bound of $\frac{3}{7} \approx 0.428571$. However, the framework was able to reproduce the following sharp results.

Theorem (Ben-Haim and Litsyn). The minimum density of an identifying code in the square grid is $\frac{7}{20}$.

Theorem (Karpovsky, Chakrabarty, and Levitin). The minimum density of an identifying code in the triangular grid is $\frac{1}{4}$.

Theorem (Honkala). The minimum density of a locating-dominating code in the hexagonal grid is $\frac{1}{3}$.

Theorem (Slater). The minimum density of a locating-dominating code in the square grid is $\frac{3}{10}$.

Theorem (Seo and Slater). The minimum density of an OLD code in the hexagonal grid is $\frac{1}{2}$.

Theorem (Seo and Slater). The minimum density of an OLD code in the square grid is $\frac{2}{5}$.

Theorem (Kincaid, Oldham, and Yu). The minimum density of an OLD code in the triangular grid is $\frac{4}{13}$.

Research Papers
D. Stolee, Automated Discharging Arguments for Density Problems in Grids (Extended Abstract) submitted.
Web Version ArXiv Version
Software

The ADAGE Framework is available as open-source software. You can find the most-recent version at the GitHub page or at my software web page. You can also download the software here:

Related Work
Y. Ben-Haim and S. Litsyn. Exact minimum density of codes identifying vertices in the square grid. SIAM Journal on Discrete Mathematics, 19(1):69-82, 2005.
A. Cukierman, G. Yu, New bounds on the minimum density of an identifying code for the infinite hexagonal grid Discrete Applied Mathematics 161(18) (2013) pp. 2910-2924.
I. Honkala. An optimal locating-dominating set in the infinite triangular grid. Discrete Mathematics, 306(21):2670-2681, 2006.
M. G. Karpovsky, K. Chakrabarty, and L. B. Levitin. On a new class of codes for identifying vertices in graphs. IEEE Transactions on Information Theory, 44(2):599-611, 1998.
R. Kincaid, A. Oldham, and G. Yu. Optimal open-locating-dominating sets in infinite triangular grids. arXiv preprint arXiv:1403.7061, 2014.
A. Razborov, Flag Algebras The Journal of Symbolic Logic 72(4) (2007) pp. 1239-1282
P. J. Slater. Fault-tolerant locating-dominating sets. Discrete Mathematics, 249(1):179-189, 2002.
S. J. Seo and P. J. Slater. Open neighborhood locating-dominating sets. Australasian J. Combin, 46:109-120, 2010.
Presentations
Automated Discharging Arguments for Density Problems in Grids. Connections in Discrete Mathematics: a Celebration of the Work of Ron Graham (06/19/15), Simon Fraser University.
Slides
Automated Discharging Arguments for Density Problems in Grids. Department of Mathematics Colloquium (09/02/14), Iowa State University.
Slides

Derrick Stolee - Iowa State University - Research Browser