Seminar Details

The metric dimension of the hypercube is the smallest cardinality of a set, S, of n dimensional 0/1 vectors so that any two distinct 0/1 vectors have different Hamming distances to some member of S. This problem was first treated ("Problem B") in a paper of Erdos-Renyi ("Two Problems in Information Theory") where it is closely connected with the coin weighing problem of Soderberg-Shapiro ("Problem A"). Using the probabilistic method they gave a lower bound, which combined with later explicit constructions by Cantor-Mills and Lindstrom give tight asymptotics. However finding the exact value has been challenging. It is detailed in OEIS sequence A303735. There have a been a number of papers devoted to this problem, but almost all of them use heuristic search to find smaller sized sets S than those given by the explicit constructions, and do not deal with certifying that the set, S, is minimal.

In this talk I'll discuss the use of SAT solvers which allowed calculation of three new values using the CEGAR (counter-example guided abstraction refinement) method. In the course of this investigation a number of auxilliary problems arose: (1) Using a refinement of entropy inequalities of Pippenger to drastically cut down on the number of cases needed to be handled. (2) A related problem of finding the minimum subset of 0/1 vectors required in order to certify a minimal S. (3) Giving short "certificates" asserting that the computation is correct.