Verified Certificates via SAT and Computer Algebra Systems for the Ramsey R(3,8) and R(3,9) Problems

1 Introduction

Ramsey Theory studies the existence of substructures with order within sufficiently large structures. The classical Ramsey R(3, k) problem seeks the smallest integer n (known as the Ramsey number) such that any red/blue edge coloring of the complete graph on n vertices must contain either a blue triangle or a red k-clique. This problem is often framed as the "party problem": determining the minimum number of guests required to ensure that either three guests all know each other or k guests are mutual strangers. Despite its simple formulation, computing Ramsey numbers is notoriously difficult, with only nine non-trivial values known to date, despite extensive research.

Most contemporary methods of finding non-trivial Ramsey numbers rely heavily on the use of computer programs such as NAUTY [McKay and Piperno, 2014] to enumerate graphs exhaustively. However, NAUTY cannot generate a formal certificate certifying that the enumeration is indeed exhaustive, thus raising the possibility that these results may have errors in them. In this paper, we apply MATHCHECK [Zulkoski et al., 2015] and combine satisfiability solvers with computer algebra systems (SAT+CAS) [Bright et al., 2022] to not only produce formal certificates for Ramsey numbers but also achieve significant speedups compared to SAT-only approaches. A key component of our implementation is the use of the IPASIR-UP interface [Fazekas et al., 2023] that facilitates seamless integration of external learned clause addition within modern SAT solvers. Specifically, we leverage IPASIR-UP to implement the CADICAL+CAS framework as part of MATHCHECK. In this work, we focus on providing certificates of completeness for the exhaustive search components required to determine R(3, k) and R(k, 3). It is important to emphasize that our approach does not constitute a formal proof of the Ramsey number. Instead, our certificates ensure correctness and completeness for the parts of the proof involving exhaustive graph enumeration. To follow the established convention in Ramsey theory, this paper begins by discussing the Ramsey number R(3, k). In later sections we find R(k, 3) aligns better with our computational approach, but R(3, k) = R(k, 3), as these are symmetric by definition.

1.1 Our Contributions

1) Certified Ramsey numbers: In this paper, we extend the well-known SAT+CAS tool MATHCHECK [Zulkoski et al., 2015] (see Figure 1) to solve Ramsey problems of type R(3, k) and R(k, 3), and provide certificates of correctness. 1 These certificates ensure the correctness of the exhaustive search process, though we cannot claim complete formal proofs since the SAT encodings have not been formally verified. We verify the values of two Ramsey numbers for k = 8 [McKay and Min, 1992] and k = 9 [Grinstead and Roberts, 1982], whose proofs rely heavily on graph enumeration. To our knowledge, these are the only two known Ramsey numbers that have not been verified with proof certificates.

1 All results can be reproduced using the public code from https: //github.com/ConDug/MathCheckRamsey.

2) Speedup over SAT-only approaches: We show that our sequential and parallel SAT+CAS tools significantly outperform SAT-only approaches (see Table 2). This speedup is achieved through the isomorph-free exhaustive generation technique employed by MATHCHECK, which reduces the search space by dynamically blocking symmetric branches.

3) Parallel cube-and-conquer SAT+CAS MATHCHECK:

We introduce a parallel cube-and-conquer SAT+CAS tool by integrating ALPHAMAPLESAT [Jha et al., 2024] as the cubing solver and MATHCHECK as the conquering solver. We solved and certified R(8, 3) = 28 in 8 hours of wall clock time, and in doing so decreased the total CPU time spent solving to 6.2 hours (while the sequential version spent 18.5 hours just solving), and solved and verified R(9, 3) = 36 in 26 hours (while the sequential version timed out after 7 days).

2 Preliminaries

2.1 SAT+CAS for Combinatorial Problems

A conflict-driven clause learning (CDCL) [Marques-Silva et al., 2021; Marques-Silva and Sakallah, 1999; Bayardo Jr. and Schrag, 1997] satisfiability (SAT) solver takes as input a Boolean formula in conjunctive normal form (CNF) and determines whether there exists an assignment of variables making the formula evaluate to true, in which case the formula is satisfiable (SAT). Otherwise, the formula is unsatisfiable (UNSAT). Thanks to the rich advancement made by the SAT community, state-of-the-art CDCL SAT solvers can solve many instances with millions of variables efficiently. However, SAT solvers face challenges when solving hard combinatorial problems such as the Ramsey problem due to the large amount of symmetry in the search space.

Computer Algebra Systems (CASs) like Maple [Bernardin et al., 2024], Mathematica [Wolfram, 2003], Magma [Bosma et al., 1997], and SageMath [Stein and Joyner, 2005] are storehouses of mathematical knowledge, containing state-ofthe-art algorithms frommany mathematical areas. Therefore, many mathematical constraints can be easily expressed in a CAS, whereas an off-the-shelf SAT solver is limited to expressions in Boolean logic.

Both SAT and CAS have their drawbacks when solving combinatorial problems. SAT solvers can perform scalable searches but lack the mathematical domain knowledge required to prune out symmetries in the search space. On the other hand, CASs have rich mathematical capabilities but lack scalability when dealing with enormous search spaces. To combine the best of both worlds, we leverage MATHCHECK to dynamically provide mathematical context to the SAT solver to only enumerate non-isomorphic graphs in the search space. Specifically, we use a CAS to generate blocking clauses that are passed to the SAT solver dynamically via a programmatic interface. These clauses block the SAT solver from exploring symmetric branches of the search tree (see Section 5). The SAT+CAS paradigm has been applied to solving hard combinatorial problems such as the Williamson conjecture [Bright et al., 2020], Lam's problem [Bright et al., 2021], the Erd˝os-Faber-Lov´asz Conjecture [Kirchweger et al., 2023a], the Kochen-Specker problem [Li et al., 2024; Kirchweger et al., 2023b], and integer factorization [Ajani and Bright, 2024]. We show that SAT+CAS is orders of magnitude faster than a SAT-only approach without compromising the verifiability of the result.

2.2 Ramsey Problems

Ramsey's theorem states that for every p, q ∈ N, there exists an n ∈ N such that every graph of order n contains either a p-clique or an independent set of size q. An m-clique is a complete subgraph of order m and an independent set is a subset of mutually unconnected vertices. The Ramsey problem is defined as finding the smallest integer n, denoted as R(p, q), for some given p and q. A common and equivalent reformulation is as follows: for every p, q ∈ N, there exists an n ∈ N such that any red/blue coloring of the edges of the complete graph of order n, denoted Kn, contains a blue monochromatic p-clique or a red monochromatic q-clique. A Ramsey (p, q)-graph is a graph without a p-clique and without an independent set of size q. Ramsey (p, q; n)-graphs and (p, q; n; e)-graphs are (p, q)-graphs on n vertices and (p, q)- graphs on n vertices with e edges, respectively. All graphs are assumed to be simple and undirected unless stated otherwise.

2.3 Correctness of Results

Correctness of results is a long-standing problem in the field of computer-assisted proofs, particularly for results that require extensive enumeration that cannot be checked by hand. Verification is of utmost importance, as it provides a formal guarantee that the result is correct. Without verification, one has to trust the correctness of the program, and this could allow undetected software or administrative errors to compromise the validity of the proof. For example, recent work uncovered consistency issues in previous computational resolutions of Lam's problem, highlighting the difficulty of relying on search code for nonexistent results [Bright et al., 2021]. For prominent combinatorial problems such as Ramsey problems relying on extensive computations, formal verification is a way to increase trust in the results.

3 Previous Work

3.1 Classical Ramsey Numbers

Gauthier and Brown (2024) formally proved R(4, 5) = 25 using a SAT solver, verifying a result originally obtained in 1995 using computational search [McKay and Radziszowski, 1995]. Gauthier and Brown's approach combined an interactive theorem prover, a SAT solver, and gluing together generalizations of colored graphs as described below. Graph gluing refers to inserting an n × n adjacency matrix and an m × m adjacency matrix along the main diagonal of a larger empty matrix, to form an (m + n) × (m + n) adjacency matrix. The remaining off-diagonal entries are then filled in subject to some constraints (in this case the Ramsey constraints) in an exhaustive way. A generalization of a colored graph is a colored graph with some edges uncolored. A (p, q)-graph generalization with one uncolored edge represents the (p, q)- graph where the uncolored edge can be colored red or blue. They constructed exact covers for sets of (3, 5; m)-graphs and (4, 4; n)-graphs, reducing the number of graph gluings required. Their method took over 2.5 years of CPU time, but they estimate it would have taken 44 years without generalizations. This represents a very recent advancement in the formal verification of results concerning Ramsey numbers, showcasing the potential of certifiable computational methods.

Fujita et al. (2013) used a soft-constraint approach to improve the lower bound of R(4, 8) from 56 to 58. They introduced two types of soft constraints: zebra soft-constraints and unit soft-constraints. These could be iteratively removed, with their selection based on the number of conflicts relating to a soft-constraint. This allowed for efficient propagation of edge assignments and significantly reduced the search space.

SAT Modulo Symmetries (SMS) is a framework developed for graph generation and enumeration [Kirchweger and Szeider, 2021]. It leverages the SAT solver CADICAL [Biere et al., 2024] with a dedicated symmetry propagator to check the canonicity of partial solutions. SMS is implemented using the IPASIR-UP interface [Fazekas et al., 2023], which allows the integration of user-defined symmetry propagators directly into the solving process, enabling efficient dynamic symmetry-breaking constraints. This approach has been applied to verify smaller Ramsey numbers, such as R(3, 5) and R(4, 4) [Kirchweger and Szeider, 2024], but has not yet been extended to larger instances. SMS uses a row-wise lexicographic ordering of the adjacency matrix for comparing graphs, whereas our method uses a column-wise ordering of edge variables above the diagonal-our method requires the latter ordering because of a particular property not satisfied by the ordering used by SMS (see Property 2 in Section 5). In addition, SMS performs canonicity checks on partially defined graphs during the solving process, while our approach only performs canonicity checks on fully defined subgraphs (whenever an upper-left submatrix becomes fully known). We opted for SAT+CAS due to the availability of its verification capability, which is not currently provided in the SMS repository.

More recently, Codel et al. (2024) introduced verified proof checking tools for the substitution redundancy (SR) proof system [Buss and Thapen, 2021; Gocht and Nordstr ¨om, 2021; Rebola-Pardo, 2023], a powerful generalization of the propagation redundancy (PR) [Heule et al., 2020] and resolution asymmetric tautology (RAT) proof systems [J¨arvisalo et al., 2012; Heule and Biere, 2018; Wetzler et al., 2014]. Their work presents the first verified SR proof checker, implemented in the LEAN theorem prover [de Moura et al., 2015], and demonstrates SR's ability to produce significantly shorter proofs than RAT for certain problems. They provide a concise 38-clause SR proof of R(4, 4) ≤ 18. Their experimental results show SR proofs are on average 99.6% smaller than equivalent RAT proofs, while their verified checker performs comparably to existing fast PR checkers. Although no current state-of-the-art SAT solvers support SR reasoning, this work lays the groundwork for potential advancements in SAT solving techniques, offering a path to more powerful reasoning and shorter proofs for complex problems.

3.2 Tri-color Ramsey Problems

An (r1, . . . , rk; n) Ramsey colouring is an edge k-coloring of Kn with no monochromatic Kri in color i. The multicolor Ramsey number R(r1, . . . , rk) is the smallest n such that no such coloring exists. Codish et al. (2016) resolved the long-standing open problem R(4, 3, 3) by showing that no (4, 3, 3; 30) coloring exists. They partitioned the search space into six ⟨a, b, c⟩-regular cases, where each vertex has fixed degrees in the three colors

All cases were proven unsatisfiable via SAT solving except ⟨13, 8, 8⟩. For that case, they generated all 3-colorings of K13 without monochromatic triangles and attempted to extend each to K30. The full computation required 128 CPU years, parallelized across 456 threads.

3.3 Directed Ramsey Graphs

A tournament is a directed graph where for every pair of vertices, exactly one directed edge exists. A tournament is transitive if for all vertices u, v, and w, the presence of edges uv and vw implies the existence of uw. The directed Ramsey number R(k) is the smallest number of vertices such that every tournament on that many vertices contains a transitive subtournament of size k.

Neiman et al. (2022) improved the known bounds on R(7) to 34 and 47 using SAT solving. For the upper bound, they encoded tournaments avoiding transitive subtournaments of size 7 and exhaustively searched all possibilities up to 46 vertices. For the lower bound, they applied a SAT solver to show no 33-vertex transitive-free tournament exists. Their approach combined constraint encodings with techniques such as self-subsuming resolution.

3.4 Previous Work on R(3, 8) and R(3, 9)

McKay and Min (1992) computationally showed R(3, 8) = 28. Their method involved generating all graphs up to isomorphism on 20-22 vertices without 3-cliques and without independent sets of size 7. They used a recursive generation procedure and the graph isomorphism tool NAUTY to remove isomorphic graphs.

Graver and Yackel (1968) made significant progress on R(3, 9) before the problem was ultimately solved by Grinstead and Roberts (1982). Graver and Yackel proved R(3, 9) ≥ 35 and showed a (3, 9; 36)-graph must be regular of degree 8 and must contain a (3, 8; 27; 80)-subgraph. Grinstead and Roberts computationally showed that no (3, 8; 27; 80)-graphs exist, thereby proving R(3, 9) = 36. Their method involved a series of lemmas on the structure of various subgraphs of (3, 8; 27; 80)-graphs and used graph gluing techniques combined with computational searches.

Since the previous approaches to R(3, 8) and R(3, 9) relied on uncertifiable computational methods for graph enumeration, we therefore present certifiable proofs using the SAT+CAS paradigm.

4 Encoding Ramsey Problems

We now discuss the encodings we used to translate the Ramsey problem into formulas in conjunctive normal form (CNF). In addition to the direct encoding of Ramsey graphs, we introduce encodings that further narrow down the search space by limiting symmetries, vertex degrees, and the number of edges in the graph.

4.1 Encoding Ramsey Graphs

The Ramsey problem is encoded for a predefined n, p, and q by deriving a Boolean formula in conjunctive normal form asserting the existence of a Ramsey (p, q)-graph of order n. The encoding enforces every p-clique to have at least one edge in the opposing (red) color and every q-clique to have at least one edge in the opposing (blue) color, i.e.,

where the variable e is assigned true (⊤) when the corresponding edge is colored blue and is assigned false (⊥) when the corresponding edge is colored red. A satisfying assignment of the encoding corresponds to finding a (p, q)-graph of order n, and therefore R(p, q) > n. Similarly, an unsatisfiable result means no such colorings exist for this particular n, i.e., all colorings contain a blue p-clique or a red q-clique, and therefore R(p, q) ≤ n.

4.2 Symmetry Breaking Constraints

In order to break the symmetries of the problem, we first add static constraints enforcing a lexicographic ordering on rows of the graph's adjacency matrix. After that, we use the dynamic symmetry breaking capabilities of a CAS to break the remaining symmetries.

The partial static symmetry breaking constraints were developed by Codish et al. (2019). These enforce a lexicographical ordering on the rows of a graph's adjacency matrix and block the solver from exploring certain symmetric portions of the search space before the CAS is called. This is beneficial as there is an overhead associated with calling the CAS.

These clauses are constructed in the following manner: for an adjacency matrix A of a graph of order n, define Ai,j as the ith row of A without columns i and j. The clauses enforce that Ai,j is lexicographically equal or less than Aj,i for all 1 ≤ i < j ≤ n. These clauses introduce O(n3 ) auxiliary variables and clauses. Based on our empirical evidence, these constraints provide a significant speed-up by breaking symmetries statically and were included in all instances.

4.3 Cardinality Constraints

Cardinality constraints are used to further reduce the search space by limiting both the degree of vertices and the number of edges in Ramsey graphs. Specifically, it is known that every vertex v of a Ramsey (p, q; n)-graph satisfies

where degb(v) is the number of blue edges on vertex v [Graver and Yackel, 1968]. We also leverage theoretical results to restrict the number of edges allowed in the Ramsey graph when proving the value of R(3, 9) in Section 7.

We encoded these constraints using the totalizer encoding of Bailleux and Boufkhad (2003). The totalizer uses a binary tree to create relationships between auxiliary variables. Each node in the tree is assigned a value and a set of unique variables. Suppose we wish to encode between l and u of m variables are true. We form a binary tree with m leaf nodes and associate each leaf node to one of these variables. For a non-leaf node r with children a, b, let R = {r1, . . . , rm0 }, A = {a1, . . . , am1 }, and B = {b1, . . . , bm2 } be the set of variables assigned to r, a and b respectively. The following conjunction of clauses is related to the node r:

with a0, b0, and r0 assigned true and am1+1, bm2+1, and rm0+1 assigned false. These clauses ensure that the number of variables assigned true in R is equal to the number of variables assigned true in A ∪ B. Finally, the clauses ∧1≤i≤l ci and ∧u+1≤i≤m ¬ci specify that between l and u of our original m variables are true where c1, . . . , cm denote the variables associated with the root node of the tree. This encoding uses O(m log m) new variables and O(mu) clauses after applying unit propagation and removing satisfied clauses.

5 Orderly Generation Using SAT+CAS

When searching for graphs using a SAT solver, the static symmetry breaking constraints introduced previously do not block all isomorphic copies-in fact, most symmetries remain in the search space. Therefore, we use a symbolic computation method to block the remaining symmetries dynamically during the solving process. Specifically, we implement an isomorph-free graph generation technique called orderly generation that was developed independently by Read (1978) and Faradˇzev (1978).

We say an adjacency matrix AG of a graph G is canonical if every permutation of the graph's vertices produces a matrix lexicographically greater than or equal to AG, where the lexicographical order is defined by concatenating the abovediagonal entries of the columns of the adjacency matrix starting from the left. In other words, the canonical matrix of a graph is the lexicographically-least (lex-least) way of representing the graph's adjacency matrix.

An intermediate matrix of AG is a square upper-left submatrix of AG. If AG is of order n then its intermediate matrix of order n - 1 is said to be its parent, and A is said to be a descendant of its intermediate matrices. The orderly generation method is based on the following two consequences of this definition of canonicity:

1. Every isomorphic class of graphs has exactly one canonical (lex-least) representative.
2. If a matrix is lex-least canonical, then its parent is also lex-least canonical.

This definition of canonicity is particularly useful as the contrapositive of the second property implies that if a matrix is not canonical, then all of its descendants are also not canonical. Therefore, any noncanonical intermediate matrix encountered during the search can be blocked immediately, as none of its descendants are canonical.

To implement the orderly generation algorithm in a SAT solver, when the solver finds a partial assignment corresponding to an intermediate matrix, the canonicity of this matrix is determined by a canonicity-checking routine implemented in the CAS (Figure 1). The CAS explores permutations of the graph's vertices and evaluates whether any of these permutations result in a lexicographically smaller adjacency matrixif so, the matrix is not canonical. If the CAS finds a permutation that demonstrates the noncanonicity of the matrix, then a blocking clause is learned which removes this matrix and all of its descendants from the search. Otherwise, the matrix is canonical and the SAT solver proceeds as normal. When a matrix is noncanonical, the canonicity-checking routine provides a witness (a permutation of the vertices producing a lex-smaller adjacency matrix), which allows for the verification of MATHCHECK's result without trusting the CAS.

Even though R(3, k) and R(k, 3) share the same value, in the context of the CNF encoding the R(3, k) and R(3, k) instances are different with R(k, 3) containing a much higher number of negative literals. An important observation in our experiments is that solving R(k, 3) is consistently faster than solving R(3, k), despite these instances being equivalent due to symmetry. This behavior persists even when the CAS is turned off (see Table 2). We solved R(3, k) and R(k, 3) for k = 8 and 9 and included both runtimes in Section 8.

6 Parallelization

In order to scale our technique up to k = 9, parallelization is used to reduce the wall clock time. We use a cube and conquer technique which splits the CNF instance into tens of thousands of subproblems and solves them in parallel.

6.1 Cube and Conquer

Cube and conquer [Heule et al., 2012] is a parallelization technique whereby a set of simpler instances are solved, and the aggregate result is equivalent to solving the original instance. Initially developed to solve SAT instances arising from computing van der Waerden numbers [Ahmed et al., 2014], many combinatorial problems have since been attacked using this technique, such as Lam's Problem [Bright et al., 2021], the Boolean Pythagorean Triples Problem [Heule et al., 2016], Schur number five [Heule, 2018], and the Kochen-Specker problem [Li et al., 2024].

Let vi be a variable appearing in the Boolean formula F. Then solving instances F1 := F ∧ vi and F2 := F ∧ ¬vi is equivalent to solving F, and if either F1 or F2 is satisfiable then F is satisfiable. We say vi is the splitting variable and consider F1 and F2 as subinstances of F. If a subinstance is still hard, an unassigned variable (subject to some selection criteria) in the subinstance can be split on. This splitting can be repeated until some stopping criteria is reached.

When choosing the appropriate cubing solver, there are two main factors to consider: one is the time it takes to generate all cubes, and the other is the quality of the cubes, which can be measured by the time required to solve the hardest cube. Two cubing solvers we tried are MARCH CU [Heule et al., 2012] and ALPHAMAPLESAT [Jha et al., 2024]. We use ALPHAMAPLESAT as it generates a large set of cubes faster without compromising the quality of the cubes.

ALPHAMAPLESAT introduces a novel approach to cube challenging combinatorial instances. At its core, ALPHAMAPLESAT employs a Monte Carlo Tree Search (MCTS) based lookahead cubing technique, setting it apart from traditional cube-and-conquer solvers. This method allows for a deeper heuristic search to identify effective cubes while maintaining low computational costs.

We define eliminated variables to be variables that are either assigned a ⊤/⊥ value or propagated to be ⊤/⊥ by a simplification solver (CADICAL with orderly generation).

To determine when to stop cubing the instance further, we used the number of eliminated variables as the stopping criteria. If the number of eliminated variables is greater than a predefined threshold, the cubing stops for this subinstance. Given the original formula ϕ, each time ALPHAMAPLESAT chooses an edge variable x to split on, the formula ϕ ∧ x and ϕ∧¬x are generated and simplified using CADICAL + CAS, so that ALPHAMAPLESAT can choose the next splitting variable based on the simplified formula, since this contains CAS-derived clauses and therefore blocking clauses from orderly generation are incorporated during the cubing process.

Following cubing, the cubes are "conquered", i.e., solved by a SAT+CAS solver. Ideally, the solver can solve all cubes. However, when our solver could not solve an instance without producing a proof file larger than 7 GiB, the instance was passed back to ALPHAMAPLESAT to be cubed again. 7 GiB was chosen as the maximum file size because we found that the DRAT-trim proof checker [Wetzler et al., 2014] could verify such proofs without exceeding our memory limit of 4 GiB. This process of alternating cubing and conquering continues for difficult instances until all cubes can be solved with proof files smaller than 7 GiB. To solve cubes efficiently across multiple CPUs, we utilized Python's multiprocessing library.

7 Theory of R(3, 9) and R(9, 3)

Directly applying a SAT+CAS solver to the R(9, 3) problem is difficult. As the problem is significantly harder than the R(8, 3) problem, we leverage theoretical results to reformulate the problem. Grinstead and Roberts (1982) combined theory and computation to show that R(3, 9) = 36, leveraging theoretical results fromGraver and Yackel (1968). This section highlights key theoretical results from Graver and Yackel's paper. The following lemma, from Section 3 of Graver and Yackel (1968), forms the basis of the original proof of R(3, 9) = 36. We also use it in our proof and verification, since the lemma does not rely on computation and can be proved mathematically.

Lemma 1. A (3, 9; 36)-graph contains a (3, 8; 27; 80)-graph. A (9, 3; 36)-graph contains a (8, 3; 27; 271)-graph.

Graver and Yackel improved the bounds on many Ramsey numbers and on the minimum number of edges in Ramsey graphs. They constructed a (3, 9)-graph on 35 vertices, thereby showing R(3, 9) > 35. Specifically for R(3, 9), Grinstead and Roberts derived a sequence of lemmas on the structures of various subgraphs of (3, 8; 27; 80)-graphs. They computationally proved structures in (3, 8; 27; 80)-graphs cannot exist in order to show R(3, 9) ≤ 36 via Lemma 1. They estimated 5 × 1010 machine operations and 2.5 × 104 seconds of computation, but note the time could be improved using machines with more efficient bitstring operations as computations were performed on a Honeywell Level 66 computer. The second part of the lemma is derived from the fact that (27 2 ) - 80 = 271, thus a (9, 3; 36)-graph contains a (8, 3; 27; 271)-graph.

We apply a parallelized SAT+CAS tool to a CNF encoding asserting the existence of a (8, 3; 27; 271)-graph. We obtained an UNSAT result (see Section 8.3), therefore showing that no (8, 3; 27; 271)-graphs exist. By Lemma 1, this implies R(9, 3) ≤ 36, and since a (3, 9; 35)-graph exists, this implies R(9, 3) = R(3, 9) = 36. In doing so, we do not rely on the method employed by the authors of the original proof to show the nonexistence of (3, 8; 27; 80)-graphs, since they rely on unverified computational results. To simplify our encoding, we do not rely on any additional theoretical results on (3, 8; 27; 80)-graphs or (8, 3; 27; 271)-graphs, aside from the vertex degree constraints mentioned in Section 4.3.

8 Results and Verification

8.1 Experimental Setup

We performed both SAT+CAS solving and verification in parallel by integrating ALPHAMAPLESAT with the MATHCHECK tool. The R(8, 3) result was obtained on a cluster of Dual Xeon Gold 6226 processors @ 2.7 GHz and used 24 CPUs, while the R(9, 3) result was computed on a cluster of Dual AMD Epyc 7713 CPUs @ 2.0 GHz and used 128 CPUs.

By default, MATHCHECK uses a pseudo-canonical check and stops the canonical check early if the CAS takes too long to determine canonicity. To optimize solving performance, we enabled full canonicity checking and this adjustment resulted in a 2× improvement in solving time. Even after enabling a full canonical check, a minority of the total solving time is spent in the CAS-for R(8, 3), the CAS accounts for 7% of the total solving time, while for R(9, 3), it accounts for 38%. Although a full canonicity check is more expensive, it generates more symmetry-blocking clauses and ultimately enhances the solver's efficiency for this problem.

Table 3 includes "simplification time" for our cube-andconquer tool. During cubing, each variable split triggers a brief CADICAL+CAS simplification (10,000 conflicts), with the simplified instance passed back to AMS. This tracks eliminated variables and crucially allows AMS to leverage CASderived clauses for balanced cube generation.

8.2 Solving R(3, 8) and R(8, 3)

The Ramsey number R(3, 8) = 28 was confirmed by obtaining an UNSAT result for the encoding asserting the existence of a 28-vertex (8, 3)-graph and a SAT result in 288 seconds for the encoding asserting the existence of a 27-vertex (8, 3)- graph. Solving R(8, 3) on 28 vertices can be done sequentially (as shown in Table 2) or in parallel.

For R(8, 3), we used the cardinality constraints from Section 4.3, implying that the degree of each vertex is between 20 and 22. Cubing was performed until 120 edge variables were eliminated. If a cube was not solved after producing a 7 GiB certificate, further cubing was applied, eliminating an additional 40 variables.

A total of 41 cubes were generated, each returning UNSAT. With parallelization, the problem was solved in approximately 8 hours of wall clock time and the combined certificate files amounted to 5.8 GiB. We applied the same techniques to solve R(3, 8), where each vertex has a degree between 5 and 7. We observed that solving the R(8, 3) instance is about 6× faster than solving R(3, 8) sequentially.

8.3 Solving R(3, 9) and R(9, 3)

Solving R(9, 3) corresponds to solving the R(8, 3; 27; 271) problem, as mentioned in Section 7. This instance must be solved using the parallelized MATHCHECK tool, as R(8, 3; 27; 271) is much more challenging to solve sequentially in a reasonable amount of wall clock time.

Cardinality constraints were applied similarly, enforcing that each vertex must have a degree between 19 and 22, and that the graph must contain exactly 271 edges. Cubing continued until 100 edge variables were eliminated. If a cube was not solved after producing a 7 GiB certificate, further cubing eliminated an additional 40 variables.

A total of 2,486 cubes were generated, each returning UNSAT. With parallelization, the problem was solved in approximately 26 hours of wall clock time and the combined proof files amounted to 289 GiB. Similarly, R(3, 9) is solved using the same cubing cutoff criteria. We witnessed that solving the R(9, 3) instance is about 6× faster than solving R(3, 9).

8.4 Verification of Results

The SAT+CAS approach produces verifiable certificates, enabling an independent third party to confirm the solver's results. These certificates ensure that the SAT solver's search is exhaustive and that the learned clauses provided by the CAS are correct. As a result, only the correctness of the proof verifier-a relatively simple piece of software-needs to be trusted, rather than the SAT solver or the CAS itself.

Verification was performed using the DRAT-trim proof checker [Wetzler et al., 2014] modified to support clauses specified to be trusted. Clauses derived from the CAS were prefixed with the character 't' to mark them as trusted, and they were verified separately. A Python script applied the witness permutations to confirm that each noncanonical adjacency matrix produced a lexicographically smaller matrix, verifying the correctness of the CAS-derived clauses. Since the script verifies that each CAS-derived clause in the DRAT proof blocks only noncanonical partial assignments, we do not rely on the correctness of the somewhat complicated canonical check in the CAS. Furthermore, this verification approach addresses the soundness of the overall search regardless of potential communication issues between the CAS and the SAT solver.

When using the cube-and-conquer approach, it is critical to ensure that the generated cubes collectively partition the search space. Completeness was verified by recursively checking that for any literal x forming a cube ϕ ∧ x, all extensions of the complementary literal ϕ ∧ ¬x were covered by the set of generated cubes. This process confirmed that R(8, 3) = R(3, 8) = 28 and R(9, 3) = R(3, 9) = 36. In addition, we ran R(8, 3) on the same machine sequentially and obtained a runtime of 66,504 seconds (see Table 3), however, the total CPU time combining cubing, simplification, and solving was only 22,388 seconds. Therefore, cube-andconquer achieved a reduction in total CPU time compared to sequential solving. This mirrors the efficiency gains observed in the Boolean Pythagorean Triples problem [Heule et al., 2016], where cube-and-conquer reduced the total solving time from 2,125 days to 2 days using 800 cores, effectively reducing the computational effort to 1,600 CPU days.

While our approach produces certificates of completeness for exhaustive search procedures, these certificates do not constitute formal proofs of the corresponding Ramsey numbers. Rather, they serve as computational validation of the most resource-intensive components of the argument, i.e., the parts which in practice cannot be checked by hand. To enable full formal verification of a Ramsey number within our pipeline, two key elements remain unverified: the correctness of the SAT encoding and the correctness of the custom script used to validate clauses generated by the CAS.

9 Conclusion

Using SAT+CAS, we significantly improve the efficiency of a SAT solver on Ramsey problems and provide the first independently-checkable proof of the result R(3, 8) = 28 of McKay and Min from 1992. We verify that R(3, 9) ≤ 36 (and therefore R(3, 9) = 36) with less dependency on theoretical results than previous approaches. This result was first shown by Grinstead and Roberts in 1982 but was never before verified by independently checkable certificates.

SAT+CAS has been demonstrated to be an effective problem-solving and verifying tool for Ramsey problems. When combined with previously known domain knowledge about Ramsey problems, the search space can be reduced and thus the effectiveness of the SAT+CAS method is improved. More difficult Ramsey problems often have larger encodings and require an excessive amount of memory. Thus, reducing problems using domain knowledge has the additional benefit of reducing the encoding size. Future applications of SAT+CAS to Ramsey problems include the verification of all known Ramsey numbers and determining the values of R(3, 10), R(4, 6), or R(5, 5), which remain open problems. While our certificates are independently checkable and ensure correctness of each individual SAT instance, a fully formal proof of the main theorem would require formalizing the correctness of the CNF encoding, verifying the checker used to validate UNSAT claims, verifying the correctness of Lemma 1, and connecting the SAT results to the formal definition of the Ramsey number in a proof assistant such as LEAN or COQ. We leave this comprehensive formalization to future work.