SAT Solvers, Isomorph-free Generation, and the Quest for the Minimum Kochen–Specker System

I will describe a new approach for exhaustively generating combinatorial objects by combining a satisfiability (SAT) solver with an isomorph-free exhaustive generation method such as orderly generation.  The SAT solver is able to limit the search to objects that satisfy given criteria, while the isomorph-free generation method ensures that the objects are generated up to isomorphism.  The combined search procedure performs orders-of-magnitude faster than a pure SAT or pure computer algebraic approach, as the SAT solver tailors the search to the object in question while the isomorph-free generation avoids duplication of work when the search space is highly symmetrical.

As a motivating example, I will discuss how this approach can be applied to search for Kochen–Specker (KS) systems, an important combinatorial object arising in quantum physics.  For example, a KS system is at the heart of the "KS Theorem" which intuitively states that a quantum observation cannot be understood as revealing a pre-existing value, and the "Free Will Theorem" which intuitively states that if humans have free will then so must quantum particles.

Since 1990, the smallest known KS system in three dimensions has contained 31 vectors and much effort has been expended trying to find a KS system of smaller size.  An exhaustive computer search in 2016 was able to disprove the existence of a KS system of 21 or fewer vectors.  Our SAT and orderly generation approach is over 25,000 times faster than the previously used approach and has also ruled out the existence of a KS system with 22 vectors.

This work is joint with Zhengyu Li and Vijay Ganesh (University of Waterloo).