  We present a new SAT-based method for generating all graphs up to isomorphism
that satisfy a given co-NP property. Our method extends the SAT Modulo Symmetry
(SMS) framework with a technique that we call co-certificate learning. If SMS
generates a candidate graph that violates the given co-NP property, we obtain a
certificate for this violation, i.e., `co-certificate' for the co-NP property.
The co-certificate gives rise to a clause that the SAT solver, serving as SMS's
backend, learns as part of its CDCL procedure. We demonstrate that SMS plus
co-certificate learning is a powerful method that allows us to improve the
best-known lower bound on the size of Kochen-Specker vector systems, a problem
that is central to the foundations of quantum mechanics and has been studied
for over half a century. Our approach is orders of magnitude faster and scales
significantly better than a recently proposed SAT-based method.
