ramsey_bug.cry

// From the paper:
// McKay, B., and S. Radziszowski. "𝑅 (4, 5)= 25." J. Graph Theory 19 (1995): 309-322. 
//
// The Ramsey Number R(s,t) is the least integer n such that for 
// every n-vertex graph, there exists either a clique of order s
// or an independent set of order t.
// 
// Note: It is impossible to calculate binomial coefficients in
// Cryptol's type system. In this implementation, we overapproximate.
// 
// Example invocation:
// :prove R`{3,5,14}
// 
// If this proof fails, it will return a counterexample graph that 
// contains no clique or independent set. Otherwise, if the proof 
// passes, then there are no such graphs.

crash = R`{3,3,5} 0b1010100011

// Returns true if the n-graph has either a clique of size s or an
// independent set of size t. Proving this for size n and disproving it
// for size < n demonstates that Ramsey number R(s,t) = n.
R : {s, t, n}
    (fin n, fin s, fin t,
    n >= s, n >= t, n >= width s, n >= width t, n >= 1, n * (n - 1) / 2 >= n) 
    => [n*(n-1)/2] -> Bit
R gv = graph_contains_s_clique || graph_contains_t_independent_set
  where
    g = graph`{n} gv
    graph_contains_s_clique = 0 != 
      parmap (\(set, valid) -> if valid then is_clique g set else False) (take`{bc n s} n_choose_k_bits`{n,s})
      // map (\(set, valid) -> if valid then is_clique g set else False) (take`{bc n s} n_choose_k_bits`{n,s})
    graph_contains_t_independent_set = 0 !=
      map (\(set, valid) -> if valid then is_independent_set g set else False) (take`{bc n t} n_choose_k_bits`{n,t})

// Generates an undirected size-n graph (in matrix form) with no loops
// given a vector of size n*(n-1)/2 representing the upper triangular
// of that graph.
graph : {n, m} (fin n, fin m, n >= 1, m >= n, m == n*(n-1)/2)
  => [m] -> [n][n]
graph v = upper || lower
  where
    is = tail [0:[width m]...] : [inf][width m]
    ls = [0] # [l+i | l <- ls | i <- reverse (take`{n-1} is)] : [n][width m]
    rs = take is : [n][width m]
    upper = [ take ((v << l) >> r) | l <- ls | r <- rs ]
    lower = transpose upper

// Assumes graph is undirected and has no loops
is_independent_set : {n} (fin n) => [n][n] -> [n] -> Bit
is_independent_set g set = result
  where
    result = ~0 == [if e then 0 == (row && set)
                    else True | e <- set | row <- g]

// Assumes graph is undirected and has no loops
is_clique : {n} (fin n, n >= 1) => [n][n] -> [n] -> Bit
is_clique g set = result
  where
    rs = [[True] # 0] # [r >> 1 | r <- rs]
    identity_matrix = (take rs):[n][n]
    g' = g || identity_matrix
    result = ~0 == [if e then set == (row && set)
                    else True | e <- set | row <- g']

// Compute the lexicographically next bit permutation
// Anderson, Sean Eron. "Bit twiddling hacks." URL: http://graphics. stanford. edu/~ seander/bithacks. html (2005).
lexigraphicallyNextBitPermutation v = w
  where
    t = (v || (v - 1)) + 1
    w = if v == 0 then 0
        else t || ((((t && -t) / (v && -v)) >> 1) - 1)

n_choose_k_bits : {n, k} (fin n, n >= 1, fin k, n >= k, n >= width k) => [inf]([n], Bit)
n_choose_k_bits = xs
  where xs = [(repeat False # repeat`{k} True, True)] #
             [((y, y != ~0 /\ y != 0) where y = (lexigraphicallyNextBitPermutation x)) | (x, _) <- xs ]

// Overapproximation of binary coefficients (n choose k <= (n*e/k)^^k)
// Das, Shagnik. "A brief note on estimates of binomial coefficients." URL: http://page. mi. fu-berlin. de/shagnik/notes/binomials. pdf (2016).
type e_approx_num = 22526049624551
type e_approx_denom = 8286870547680
type bc n k = (n * e_approx_num) ^^ k / (k * e_approx_denom) ^^ k + 1