# cocertificate_learning_with_sat_modulo_symmetries__9443428e.pdf Co-Certificate Learning with SAT Modulo Symmetries Markus Kirchweger , Tom aˇs Peitl and Stefan Szeider Algorithms and Complexity Group, TU Wien, Austria {mk, peitl, sz}@ac.tuwien.ac.at We present a new SAT-based method for generating all graphs up to isomorphism that satisfy a given co-NP property. Our method extends the SAT Modulo Symmetry (SMS) framework with a technique that we call co-certificate learning. If SMS generates a candidate graph that violates the given co-NP property, we obtain a certificate for this violation, i.e., co-certificate for the co-NP property. The cocertificate gives rise to a clause that the SAT solver, serving as SMS s backend, learns as part of its CDCL procedure. We demonstrate that SMS plus co-certificate learning is a powerful method that allows us to improve the best-known lower bound on the size of Kochen-Specker vector systems, a problem that is central to the foundations of quantum mechanics and has been studied for over half a century. Our approach is orders of magnitude faster and scales significantly better than a recently proposed SAT-based method. 1 Introduction SAT modulo symmetries (SMS) is a recently proposed framework that brings efficient symmetry breaking to conflictdriven (CDCL) SAT solvers and has achieved state-of-the-art results on several symmetry-rich combinatorial search problems, enumerating or proving the non-existence of graphs, planar graphs, directed graphs, and matroids with particular properties [Kirchweger and Szeider, 2021; Kirchweger et al., 2022; Kirchweger et al., 2023b]. In this paper, we propose to extend SMS to a class of problems that do not admit a succinct SAT encoding because they involve quantifier alternation: where we are asked to find a combinatorial object (the existential part) that has some co-NP-complete property (the universal part, stated as all candidate polynomial-size witnesses fail ). We call such problems alternating search problems; a simple concrete example of an alternating search problem is the well-studied question posed by Erd os [1967], of finding a smallest triangle-free graph that is not properly kcolorable, for a fixed k 3. Encoding the non-k-colorability property for k 3 into a family of polynomially sized propositional formulas is impossible unless NP = co-NP, since checking k-colorability is NP-complete [Karp, 1972]. SMS has some advantages over alternative methods such as isomorphism-free exhaustive enumeration by canonical construction path [Mc Kay, 1998] as implemented in tools like Nauty [Mc Kay and Piperno, 2014], or different symmetrybreaking methods for SAT. The former can very efficiently generate all objects of a given order, but is very difficult to integrate with complex constraints and learning, while the latter is either intractable (full static symmetry breaking [Codish et al., 2016; Itzhakov and Codish, 2015], which requires constraints of exponential size), or ineffective (partial static symmetry breaking [Codish et al., 2019]). Because SMS strikes a better balance than these other methods, with both native constraint reasoning and learning as well as effective and efficient symmetry breaking, we chose it as our basis for alternating search. We call our new method SMS plus co-certificate learning (CCL), and it works as follows. We run an SMS solver on an encoding of the existential part of our alternating search problem, giving us a model that corresponds to a solution candidate. In the context of our running example, this candidate would be a triangle-free graph. Next, we test the co-NP property (non-k-colorability). If the graph is not colorable, we have found a solution (and we may or may not proceed to enumerate all solutions as with any other SAT encoding). If it is colorable, we find a coloring, which is a co-certificate of the graph not having our desired non-colorability property. The co-certificate gives rise to a clause that is learned by the SMS solver and prevents any solutions with the same co-certificate (colorable by the same coloring), and search resumes. We describe the method in full detail in Section 3 for now suffice it to say that we essentially apply SMS incrementally with respect to the learned co-certificates. Co-certificate learning is a general method that applies to any alternating search problem, but it is much easier to explain on a concrete example like graph coloring. In Sections 4 and 5, we present a more involved application of CCL, to the existence of Kochen-Specker (KS) systems, a combinatorial object that features in the proof of the Bell-Kochen Specker theorem in quantum mechanics. With SMS+CCL we achieve an orders-of-magnitude speed-up over a different recently proposed SAT-based approach to the KS problem, and we prove that any KS system must have at least 24 vectors. Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence (IJCAI-23) 2 Preliminaries For a positive integer n, we write [n] = {1, 2, . . . , n}. We assume familiarity with fundamental notions of propositional logic [Prestwich, 2009]. In this paper we are presenting a general method for alternating combinatorial search problems on particular examples with graphs; below we review basic notions from graph theory relevant to our discussion. Graphs. All considered graphs are undirected and simple (i.e., without parallel edges or self-loops). A graph G consists of set V (G) of vertices and a set E(G) of edges; we denote the edge between vertices u, v V (G) by uv or equivalently vu. The order of a graph G is the number of its vertices, |V (G)|. We write Gn to denote the class of all graphs with V (G) = [n]. The adjacency matrix of a graph G Gn, denoted by AG, is the n n matrix where the element at row v and column u, denoted by AG[v][u], is 1 if vu E and 0 otherwise. Isomorphisms. For a permutation π : [n] [n], π(G) denotes the graph obtained from G Gn by the permutation π, where V (π(G)) = V (G) = [n] and E(π(G)) = { π(u)π(v) : uv E(G) }. Two graphs G1, G2 Gn are isomorphic if there is a permutation π : [n] [n] such that π(G1) = G2; in this case G2 is an isomorphic copy of G1. Coloring. A (proper) k-coloring of a graph G is a map c : V (G) [k] with the property that if uv E(G), then c(u) = c(v) (adjacent vertices have different colors). Partial graphs. A partially defined graph is a graph G where E(G) is split into two disjoint sets D(G) and U(G). D(G) contains the defined edges, U(G) contains the undefined edges. A (fully defined) graph is a partially defined graph G with U(G) = . A partially defined graph G can be extended to a graph H if D(G) E(H) D(G) U(G). SAT Modulo Symmetries (SMS). SMS is a framework that augments a CDCL (conflict-driven clause learning) SAT solver [Fichte et al., 2023; Marques-Silva et al., 2009] with a custom propagator that can reason about symmetries, allowing to search modulo isomorphisms for graphs in Gn which satisfy constraints described by a propositional formula. During search the SMS propagator can trigger additional conflicts on top of ordinary CDCL and consequently learn symmetry-breaking clauses, which exclude isomorphic copies of graphs. More precisely, only those copies which are lexicographically minimal (canonical) by concatenating the rows of the adjacency matrix are kept. A key component is a minimality check, which decides whether a partially defined graph can be extended to a minimal graph; if it cannot, a corresponding clause is learned. For a full description of SMS, we refer to the original work where the framework was introduced [Kirchweger and Szeider, 2021]. 3 Co-Certificate Learning (CCL) In this paper we propose to extend SMS to alternating search problems. The way we do this is by applying SMS incrementally. In this section we shall explain the procedure by showing how it would play out in our running example of finding a triangle-free graph with n vertices and without a k-coloring. CDCL Solver Solution Candidate Symmetry Check co-NP Check co-certificate blocking clause Figure 1: Co-certificate learning = SMS + co-NP property check. Throughout this section we will talk about propositional formulas that encode graphs with the vertices [n] using the variables eu,v, where u, v [n]. Any truth assignment α defines the (possibly partially defined) graph Gα with V (Gα) = [n] and E(Gα) = {uv : α(eu,v) = 1}). First, we generate a triangle-free graph, which is obtained from a SAT solver as a model of a (polynomial-size) propositional formula encoding triangle-freeness the clauses eu,v ev,w eu,w for u, v, w V, u < v < w forbid all triangles. We feed the candidate graph into a custom coloring algorithm and test whether it is k-colorable. We will only deal with small enough graphs that the time cost of coloring, though exponential in the worst case, is going to be negligible. On the other hand, it could be the case that candidate graphs have many colorings, and the choice of a particular coloring might matter much more. We will elaborate on this in Section 5.1. Returning to our candidate graph, if it is not colorable, we obtain a solution. Depending on whether we want just one or all solutions we can stop or add a clause blocking this particular solution and resume. If, on the other hand, the graph is k-colorable, we obtain a certificate for this in the form of a coloring c : [n] [k]. We learn and add a coloring clause u4 days 147.57 Table 1: Running times in seconds of different approaches to the -free non-colorable problem. The time for Nauty includes postprocessing to filter out 3-colorable graphs, using the same code as for the other methods. 3.2 Comparison with Alternatives For the remainder of this section, we will present an experimental comparison of SMS+CCL to various alternative methods on the task of finding non-3-colorable triangle-free graphs with 10 14 vertices, showing how we can visit fewer candidate graphs and learn small sets of colorings thanks to SMS and CCL. The methods we compare are: Nauty [Mc Kay and Piperno, 2014]: enumeration modulo isomorphism of triangle-free graphs via Nauty s builtin geng -t, followed by filtering out non-3-colorable graphs by our custom code; PSS+CCL: enumeration of triangle-free graphs with a SAT solver and with partial static symmetry breaking [Codish et al., 2019], interleaved with CCL for 3-colorability (same custom code as above, custom implementation of the symmetry breaking constraints); SMS+CCL: as described above (using the same SAT solver as PSS). Another alternative that we did not consider for this comparison is to use full static symmetry breaking, which produces a constraint of exponential size and is known to scale to no more than 12 vertices [Codish et al., 2016]. From Table 1 we can see that CCL provides a speed-up of many orders of magnitude over isomorphism-free exhaustive generation with Nauty followed by 3-colorability filtering. Table 2 explains this speed-up clearly in terms of the number of graphs that need to be enumerated. Nauty always needs to enumerate all (non-isomorphic) graphs, the number in the first column. This is many orders of magnitude larger than the number of (fully defined) graphs visited by SMS + CCL: those in the third column. Even more striking is the tiny number of colorings that are sufficient to color all canonical graphs, shown in the parentheses in the last column of Table 2. In the case of n = 14, a single 3-coloring covers almost 50000 canonical graphs on average! Incomplete static symmetry breaking on the other hand, while allowing the use of CCL, is not as good at reducing the search space, as can be witnessed by the running times and the number of graphs enumerated, as well as the total number of graphs that pass the symmetry breaking constraint, shown in Table 2. Note that in this comparison we did not tweak the details of the methods so as to extract every last bit of performance (see, e.g., the work by Goedgebeur [2020] for a high-tech Nautybased solution to the triangle-free non-colorable problem). The point of this comparison is to demonstrate the inherent Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence (IJCAI-23) n Nauty PSS PSS+CCL SMS+CCL 10 12172 309987 171 54(54) 11 105071 9969561 618 147(146) 12 1262180 3668 505(481) 13 20797002 171780 3124(2014) 14 467871369 > 2 107 85668(9407) Table 2: 1st column: the number of non-isomorphic -free graphs of order n; Nauty has to process all of them. 2nd column: the number of -free graphs with n vertices that pass the PSS constraint of Codish et al. [2019] (we did not compute the missing entries, because n = 11 already took more than 8 hours). This gives an idea of the general effectiveness of PSS visa-vis the true number of non-isomorphic graphs. 3rd and 4th column: the number of graphs visited by PSS+CCL and SMS+CCL respectively, in parentheses of the 4th column the number of colorings (co-certificates) learned by SMS+CCL; contrast this number with the vastly larger total number of graphs in the first column. limits of each of these approaches, as well as to compare the off-the-shelf versions of every method. We thus conclude that, at least in the context of alternating problems like graph coloring, co-certificate learning is absolutely crucial to prevent exhaustive enumeration, and SMS is the symmetry-breaking method that scales best. Having introduced our general framework of co-certificate learning, we shall now turn our attention to the interesting multi-faceted application that is the search for a smallest Kochen-Specker vector system. 4 Kochen-Specker Systems Kochen-Specker (KS) vector systems are specific sets of vectors in at least 3-dimensional space that form the basis of the Bell-Kochen-Specker Theorem, a central result in the foundations of quantum mechanics. The existence of a KS vector system shows that quantum mechanics is in conflict with classical models in which the result of a measurement does not depend on which other compatible measurements are jointly performed, a phenomenon known as contextuality [Budroni et al., 2022]. In their original 1967 paper, Kochen and Specker [1967] proposed a 3-dimensional KS vector system of size 117. Since then, researchers have been striving to find smaller KS vector systems and establish lower bounds on their size. KS vector systems of a higher dimension n 3 are also considered in the literature, with the additional property that any pair of vectors belongs to a set of n mutually orthogonal vectors [Paviˇci c et al., 2005]. Higher dimensions allow for smaller KS systems, whereas the additional property increases the size of smallest KS systems. In the following we focus on KS vector systems of dimension 3. The smallest KS vector system (of dimension 3) known to date is due to Conway and Kochen and has 31 vectors [Peres, 1991]. The first lower bound, of 18, was given by Arends et al. [2011]; later it was improved to 22 by Uijlen and Westerbaan [2016], and recently to 23 by Li et al. [2022]. All these lower bounds were obtained by computer search methods for undirected graphs associated with KS vector systems. Since the search space is enormous and further increases by several orders of magnitude with each increment, the methods must become more and more sophisticated. Arends et al. obtain their lower bound with backtracking search that rules out all KS vector systems with 17 or fewer vectors; Uijlen and Westerbaan improved this method by deriving additional necessary restrictions on the graphs, ruling out KS vector systems with up to 21 vectors. Li et al. propose a SAT-based method where the SAT solver interacts with a computer algebra system (CAS) and prove non-existence of KS systems with 22 vectors. We will discuss the difference between their and our approach below. We give a lower bound of 24 using SMS+CCL to exclude KS systems with up to 23 vectors. Next, we define the properties of graphs associated with KS vector systems, closely following Arends et al. s approach, which has also been adopted by subsequent authors [Uijlen and Westerbaan, 2016; Li et al., 2022]. A KS graph is a simple undirected graph which is not 010colorable but embeddable, where these two properties are defined as follows. A graph G is 010-colorable if we can assign 0 or 1 to its vertices in such a way that (i) no two adjacent vertices are both assigned 0, and (ii) vertices forming a triangle are not all assigned 1. G is embeddable if its vertices can be mapped to three-dimensional real vectors such that adjacent vertices are orthogonal and there is no collinear pair. Figure 2 shows Conway and Kochen s 31-vertex KS graph and an embedding. As shown by Arends et al. [2011], there exists a KS vector system with n vectors if an only if there exists a KS graph with n vertices. Moreover, Arends et al. give the following necessary properties of any smallest KS graph G: 1. G is square-free (i.e., has no cycle of length 4); 2. G is 4-colorable; 3. G has minimum degree at least 3; 4. each vertex of G belongs to a triangle. Non-010-colorable graphs satisfying the previous four necessary properties are called KS candidates. They are only candidates , because they are not guaranteed to be embeddable. All known lower bounds on the size of a KS system were obtained by enumerating all KS candidates (modulo isomorphisms), and checking that none are embeddable. We now turn to the description of our own process for proving KS lower bounds, which also follows this two-phase pattern, but differs in our use of the new SMS+CCL method for the enumeration phase, and in some aspects of the embeddability check. We note that checking non-010-colorability is co-NP-complete [Arends et al., 2011], hence this property is well-suited for our method. 5 New Lower Bound for KS Systems This section is devoted to a description of our SAT encoding for the search of KS graphs, followed by a discussion of experimental results. We first produce a formula Fn, whose non-010-colorable models correspond to KS candidates; we then enumerate the non-010-colorable models of Fn with SMS+CCL; and finally we check the obtained graphs for embeddability. Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence (IJCAI-23) 3 13 11 31 19 23 7 17 22 5 18 4 21 2 20 Figure 2: Top: smallest known KS graph with 31 vertices and 71 edges, drawn properly 4-colored. Bottom: an embedding of this graph, where each vertex corresponds to a vector starting at the center of the cube. For instance, the vertices 1 and 30 are adjacent, and hence their corresponding vectors ( 1, 2, 1) and (2, 0, 2), respectively, are indeed orthogonal (i.e., perpendicular) since 1 2 + 2 0 + 2 1 = 0. 5.1 Encoding and CCL We use the variables ev,u to indicate whether a certain edge is present (edge variables) and the auxiliary variables tv1,v2,v3 indicating whether v1, v2, v3 forms a triangle. A graph can be extracted from a model of Fn by looking at the assignment of the edge variables. Our encoding is almost identical to previous work [Li et al., 2022] with the exception that coloring clauses are learned lazily. The necessary conditions mentioned at the end of Section 4 are encoded as follows: 1. ev1,v2 ev2,v3 ev3,v4 ev1,v4 for v1, v2, v3, v4 [n] where vi = vj if i = j and v1 < v2 < v4, v1 < v3, to forbid only one orientation of each 4-cycle. 2. To express that G must be 4-colorable, we need additional variables cv,i, v [n], i [4], for the color of each vertex. To ensure each vertex is colored we add the clauses W i [4] cv,i for v [n], and to avoid monochromatic edges we add ev,u cv,i cu,i for i [4]. 3. To enforce minimum degree at least 3, we use sequential counters [Sinz, 2005]. 4. The clauses W v2,v3 [n]\{v1},v2