
SAT Solvers, Isomorphfree Generation, and the Quest for the Minimum Kochenâ€“Specker SystemCurtis Bright, University of Windsor
Abstract: I will describe a new approach for exhaustively generating combinatorial objects by combining a satisfiability (SAT) solver with an isomorphfree exhaustive generation method such as orderly generation. The SAT solver is able to limit the search to objects that satisfy given criteria, while the isomorphfree generation method ensures that the objects are generated up to isomorphism. The combined search procedure performs ordersofmagnitude faster than a pure SAT or pure computer algebraic approach, as the SAT solver tailors the search to the object in question while the isomorphfree 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 preexisting 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). 