  A non-redundant integer cone generator (NICG) of dimension $d$ is a set $S$
of vectors from $\{0,1\}^d$ whose vector sum cannot be generated as a positive
integer linear combination of a proper subset of $S$. The largest possible
cardinality of NICG of a dimension $d$, denoted by $N(d)$, provides an upper
bound on the sparsity of systems of integer equations with a large number of
integer variables. A better estimate of $N(d)$ means that we can consider
smaller sub-systems of integer equations when solving systems with many integer
variables. Furthermore, given that we can reduce constraints on set algebra
expressions to constraints on cardinalities of Venn regions, tighter upper
bound on $N(d)$ yields a more efficient decision procedure for a logic of sets
with cardinality constraints (BAPA), which has been applied in software
verification. Previous attempts to compute $N(d)$ using SAT solvers have not
succeeded even for $d=3$. The only known values were computed manually:
$N(d)=d$ for $d < 4$ and $N(4) > 4$. We provide the first exact values for $d >
3$, namely, $N(4)=5$, $N(5)=7$, and $N(6)=9$, which is a significant
improvement of the known asymptotic bound (which would give only e.g. $N(6) \le
29$, making a decision procedure impractical for $d=6$). We also give lower
bounds for $N(7)$, $N(8)$, $N(9)$, and $N(10)$, which are: $11$, $13$, $14$,
and $16$, respectively. We describe increasingly sophisticated specialized
search algorithms that we used to explore the space of non-redundant generators
and obtain these results.
