There are a number of ways of generating combinatorial objects “up to isomorphism” [6]. An approach often used in the satisfiability (SAT) community removes isomorphic solutions from the search via the addition of new constraints [2]. Alternatively, an approach in the symbolic computation community iteratively constructs objects using an isomorph-free method such as orderly generation [4,7]. Coupling satisfiability checking with isomorph-free exhaustive generation has been explored recently [1,5,8].

We use SAT solving and orderly generation to search for Kochen–Specker (KS) systems—a crucial ingredient used in the proof of the “Free Will Theorem” that if humans have free will then so do elementary particles [3]. We show that augmenting a SAT solver with orderly generation dramatically improves its performance, especially as the size of the search increases. Our search for KS systems of size 21 is over a thousand times faster than the previous best approach [9] and we derive a new lower bound by showing a KS system must be of size 23 or greater.

References
[1] C. BRIGHT; K. K. H. CHEUNG; B. STEVENS; I. KOTSIREAS; V. GANESH. A SAT-based resolution of Lam’s problem. In Proceedings of the Thirty-Fifth AAAI Conference on Artificial Intelligence, pages 3669–3676, 2021.
[2] M. CODISH; A. MILLER; P. PROSSER; P. J. STUCKEY. Constraints for symmetry breaking in graph representation. Constraints, 24(1):1–24, 2019.
[3] J. CONWAY; S. KOCHEN. The free will theorem. Foundations of Physics, 36(10):1441–1473, 2006.
[4] I. A. FARADŽEV. Constructive enumeration of combinatorial objects. In Problèmes combinatoires et théorie des graphes, pages 131–135, 1978.
[5] T. JUNTTILA; M. KARPPA; P. KASKI; J. KOHONEN. An adaptive prefix assignment technique for symmetry reduction. Journal of Symbolic Computation, 99:21–49, 2020.
[6] P. KASKI; P. R. J. ÖSTERGÅRD. Classification Algorithms for Codes and Designs. Springer-Verlag, 2006.
[7] R. C. READ. Every one a winner or how to avoid isomorphism search when cataloguing combinatorial configurations. Annals of Discrete Mathematics, 2:107–120, 1978.
[8] J. SAVELA; E. OIKARINEN; M. JÄRVISALO. Finding periodic apartments via Boolean satisfiability and orderly generation. In Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pages 465–482, 2020.
[9] S. UIJLEN; B. WESTERBAAN. A Kochen-Specker system has at least 22 vectors. New Generation Computing, 34(1-2):3–23, 2016.