SAT + NAUTY: Orderly Generation of Small Kochen-Specker Sets Containing the Smallest State-independent Contextuality Set

TL;DR

This paper introduces a novel SAT-based orderly generation framework with recursive canonical labeling for efficiently enumerating small Kochen-Specker sets in dimension 3, achieving the first exhaustive enumeration up to 33 rays.

Contribution

The authors develop a new RCL-integrated SAT approach that overcomes exponential scaling issues, enabling exhaustive enumeration of KS sets with up to 33 rays.

Findings

First exhaustive enumeration of KS sets with up to 33 rays.

Identified the smallest 3D KS set containing the complete 25-ray SI-C set.

Verified non-existence of smaller sets with proof certificates.

Abstract

We present a search for small Kochen-Specker (KS) sets in dimension 3, specifically targeting extensions of the 13-ray Yu-Oh set, which has been proven to be the minimal witness to state-independent contextuality. To enable this search, we introduce a novel SAT-based orderly generation framework integrating recursive canonical labeling (RCL) with the graph isomorphism tool NAUTY. We demonstrate that previous SAT approaches relying on lexicographical canonicity suffer from exponential scaling on canonical graphs. This limitation renders them intractable on the large instances (25 to 33 vertices) encountered in our search, whereas our RCL check maintains consistent millisecond-level performance, effectively eliminating the bottleneck. Overcoming this bottleneck allows us to perform the first exhaustive enumeration of all KS sets with up to 33 rays containing the complete 25-ray state-independent contextuality (SI-C) set obtained by rigid extensions of the Yu-Oh set in 1,641 CPU hours. We found and verified that the 33-ray set discovered by Sch\"utte is the smallest three-dimensional KS set containing the complete 25-ray SI-C set. All non-existence results are backed by independently verifiable proof certificates via an extension of the DRAT proof format.