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

Curtis Bright, University of Windsor

11:30am Wednesday February 8th, 2023 in K9509.

Abstract:

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).