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.

翻译：我们提出了一种基于SAT的新方法，用于生成满足给定共NP性质且在同构意义下互异的所有图。该方法将SAT模对称性框架与一种称为共证书学习的技术相结合。当SMS生成违反给定共NP性质的候选图时，我们会获得该违规的证书，即该共NP性质的共证书。该共证书产生一个子句，作为SMS后端的SAT求解器会将其作为其冲突驱动子句学习过程的一部分进行学习。我们证明，SMS加上共证书学习是一种强大的方法，能够改进科亨-施佩克向量系统规模的已知最佳下界——该问题在量子力学基础中具有核心地位，且已历经半个多世纪的研究。相较于近期提出的基于SAT的方法，我们的方法速度快数个数量级，且具有显著更优的扩展性。