CNF Ramsey

Git repository

Ramsey’s theorem

Ramsey’s theorem is a theorem in combinatorics which states that a sufficiently large colored complete graph will contain a monochromatic clique. A complete graph on $n$ vertices, denoted $K_n$, has exactly $1$ edge between every vertex. An $r$-clique is a $K_r$ subgraph. The problem is to determine the minimum order complete graph that, when colored with $2$ colors, guarantees either a monochromatic $r$-clique in the first color, or $s$-clique in the second. Solutions to this problem are Ramsey numbers, and solve $R(r,s)$ for a given $r$ and $s$.

Extensions of the problem exist which consider coloring cliques of different order (edges are $1$-cliques), and using $n$ colors and cliques.

A special case exists when r=s, which is the version of the problem I solve.

2-colour case proof without words. Due to the pigeonhole principle, there are at least 3 edges of the same colour (dashed purple) from an arbitrary vertex v. Calling 3 of the vertices terminating these edges x, y and z, if the edge xy, yz or zx (solid black) had this colour, it would complete the triangle with v. But if not, each must be oppositely coloured, completing triangle xyz of that colour.

Known Ramsey numbers/bounds

Source

A complete graph on n vertices will have $n(n-1)/2$ edges. And the number of colorings is the number of colors raised to the power of the number of edges. Thus, this problem gets very unwieldy very fast, and only bounds are known as early as $R(5,5)$.

Erdős asks us to imagine an alien force, vastly more powerful than us, landing on Earth and demanding the value of $R(5, 5)$ or they will destroy our planet. In that case, he claims, we should marshal all our computers and all our mathematicians and attempt to find the value. But suppose, instead, that they ask for $R(6, 6)$. In that case, he believes, we should attempt to destroy the aliens.

-Joel Spencer

SAT solvers

SAT solvers, or Boolean satisfiability solvers, are programs that solve the boolean satisfiability problem. That is, given a statement written in boolean algebra on some variables, they determine whether there exist truth values (true or false) the variables can hold that will make the statement true. The general form of this problem is NP-complete. In fact, it is the example I would use to describe NP-complete problems. There are special grammars that allow assumptions to be made that result in much more efficient methods becoming available to solve the statement. However, Ramsey’s theorem can’t be written in any such grammar to my knowledge (I did try everything I could find).

Conjunctive normal form, or CNF, is a grammar commonly understood by SAT solvers that can encode any boolean algebra statement. The grammar uses the operators NOT, OR, and AND. Variables can be negated, a collection of variables can be ORed, and a collection of OR statements can be ANDed.

Example:

$$(A \lor \neg B \lor C) \land (\neg A \lor D)$$

In the DIMACS format, this is

p cnf 4 2
1 -2 3 0
1 4 0

Ramsey’s theorem as boolean algebra

We consider the 2-color form of Ramsey’s theorem in which edges are colored and $r=s$. The size of the complete graph $n$ and the clique size $r$ are provided as parameters to check.

The question can be rephrased to ask whether there exists a coloring of an $n$-vertex complete graph such that every $r$-clique is not monochromatic. We consider our colors to be “true” and “false”. In CNF form this is equivalent to “for every clique, at least one edge is true AND at least one edge is false”. Any coloring that makes this statement true is a counterexample to the tested value being a Ramsey number for a given clique size. A lack of counterexamples implies the tested value is at least as large as the Ramsey number for a given clique size.

In DIMACS format, a 3-clique would look like

p cnf 3 2
1 2 3 0
-1 -2 -3 0

We can generate the problem statement by:

1. Finding every $r$-clique in an $n$-vertex complete graph.
2. Numbering each edge
3. Creating a statement for every clique
4. Concatenating all statements
5. Evaluating the statement using a SAT solver

I used networkx to find the $r$-cliques:

import networkx as nx;
import itertools as it
G = nx.complete_graph('order);
def issize(val):
    return len(val)<='sclique
B = [c for c in list(it.takewhile(issize, nx.enumerate_all_cliques(G))) if len(c)=='sclique];

inline-python is used to embed this within a Rust file, and ticks precede variables pulled from outside the environment.

I numbered the edges by building a vector of ordered pairs of points and searching for matches. Creating and concatenating the statements just consisted of writing edge numbers to a string in the order they came up.

let mut edges: Vec<[u32; 2]> = Vec::new();
let cliques = c.get::<Vec<Vec<u32>>>("B");
write!(buffer, "p cnf {} {}\n", ((order * (order - 1)) / 2), 2*cliques.len())?;
for clique in cliques {
    let mut line: String = "".to_owned();
    let mut linen: String = "".to_owned();
    for a in 0..sclique {
        for b in a+1..sclique {
            let edge: [u32; 2] = [clique[a], clique[b]];
            let result = edges.iter().position(|&val| val==edge);
            let eindex = match result {
                Some(val) => val+1,
                None => {
                    edges.push(edge);
                    println!("{} = {:?}", edges.len(), edge);
                    edges.len()
                }
            };
            line.push_str(&format!("{} ", eindex).to_owned());
            linen.push_str(&format!("-{} ", eindex).to_owned());
        }
    }
    line.push_str("0\n");
    linen.push_str("0\n");
    write!(buffer, "{}", line)?;
    write!(buffer, "{}", linen)?;
}

I used cryptominisat to evaluate the statement:

c Max Memory (rss) used    : 6472 kB     
c Total time (this thread) : 0.01        
s SATISFIABLE
v -1 2 -3 -4 -5 6 7 8 9 10 -11 12 13 14 -15 -16 17 -18 -19 -20 -21 22 -23 -24 -25 
v 26 27 -28 -29 30 31 -32 -33 34 35 -36 37 38 39 -40 41 42 -43 44 -45 -46 47 48 
v 49 50 -51 -52 53 -54 -55 56 -57 58 -59 60 -61 62 -63 -64 65 -66 67 -68 69 -70 
v -71 72 -73 74 -75 -76 -77 78 -79 80 81 -82 83 84 -85 -86 -87 -88 89 -90 91 92 
v -93 -94 -95 96 97 98 99 -100 101 -102 103 104 -105 -106 107 -108 109 -110 111 
v -112 -113 114 115 116 117 -118 119 120 121 122 123 -124 -125 126 127 128 -129 
v -130 -131 -132 133 -134 -135 -136 0

Here, cryptominisat found that $R(4,4)> 17$ in $0.01$ seconds.

To understand this counterexample:

1. Label the vertices of $K_n$ however you want
2. cnf_ramsey will output numberings for edges between vertex numbers
3. cryptominisat will output whether each edge should be colored red (positive) or blue (negative). The trailing $0$ simply indicates the end of the statement.

Future Work

This program can be expanded to support more problem statements, such as $r\neq s$.

FPGA’s are basically boolean algebra accelerators. The statement can be converted to verilog, and analyzed on an FPGA for a large speed improvement. There has been research into accelerating SAT solvers using FPGAs.

A more nuanced approach can be taken utilizing both SAT solvers and CAS to generate formal proofs of the value of a given Ramsey number. Work has been done here as well.