# Co-Certificate Learning with SAT Modulo Symmetries

arXiv: https://arxiv.org/abs/2306.10427 · HTML: https://mlsanity.com/paper/2306.10427/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 1 of its 51 references that are in the map.
- First posted on arXiv 17 Jun 2023.

## Builds on (most cited first, 1 of 1)

- [Breaking Symmetries in Graph Search with Canonizing Sets](https://mlsanity.com/paper/1511.08205/) (2015)

## Built on by (most cited first, 2 of 2)

- [AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems](https://mlsanity.com/paper/2401.13770/) (2024)
- [Smart Cubing for Graph Search: A Comparative Study](https://mlsanity.com/paper/2501.17201/) (2025)

## Abstract (arXiv)

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.