Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Symbolic Sets for Proving Bounds on Rado Numbers

Tanbir Ahmed, Lamina Zaman, Curtis Bright

TL;DR

This paper advances the study of 3-colour Rado numbers for the linear equations $ax+by=bz$ and $ax+ay=bz$ by combining SAT-based computation with symbolic verification. It computes new exact values for $R_3$ in two families, derives substantial lower bounds, and proposes conjectures guided by SAT-search patterns. A key contribution is Auto-Case, a tool that automates intricate case-based proofs by manipulating symbolically-defined sets with SymPy and checking feasibility via Z3, thereby reducing human error in long proofs. The work demonstrates the viability of SC-Square approaches for Ramsey-type problems and lays groundwork for automating larger classes of Rado-number proofs.

Abstract

Given a linear equation $\cal E$ of the form $ax + by = cz$ where $a$, $b$, $c$ are positive integers, the $k$-colour Rado number $R_k({\cal E})$ is the smallest positive integer $n$, if it exists, such that every $k$-colouring of the positive integers $\{1, 2, \dotsc, n\}$ contains a monochromatic solution to $\cal E$. In this paper, we consider $k = 3$ and the linear equations $ax + by = bz$ and $ax + ay = bz$. Using SAT solvers, we compute a number of previously unknown Rado numbers corresponding to these equations. We prove new general bounds on Rado numbers inspired by the satisfying assignments discovered by the SAT solver. Our proofs require extensive case-based analyses that are difficult to check for correctness by hand, so we automate checking the correctness of our proofs via an approach which makes use of a new tool we developed with support for operations on symbolically-defined sets -- e.g., unions or intersections of sets of the form $\{f(1), f(2), \dotsc, f(a)\}$ where $a$ is a symbolic variable and $f$ is a function possibly dependent on $a$. No computer algebra system that we are aware of currently has sufficiently capable support for symbolic sets, leading us to develop a tool supporting symbolic sets using the Python symbolic computation library SymPy coupled with the Satisfiability Modulo Theories solver Z3.

Symbolic Sets for Proving Bounds on Rado Numbers

TL;DR

This paper advances the study of 3-colour Rado numbers for the linear equations and by combining SAT-based computation with symbolic verification. It computes new exact values for in two families, derives substantial lower bounds, and proposes conjectures guided by SAT-search patterns. A key contribution is Auto-Case, a tool that automates intricate case-based proofs by manipulating symbolically-defined sets with SymPy and checking feasibility via Z3, thereby reducing human error in long proofs. The work demonstrates the viability of SC-Square approaches for Ramsey-type problems and lays groundwork for automating larger classes of Rado-number proofs.

Abstract

Given a linear equation of the form where , , are positive integers, the -colour Rado number is the smallest positive integer , if it exists, such that every -colouring of the positive integers contains a monochromatic solution to . In this paper, we consider and the linear equations and . Using SAT solvers, we compute a number of previously unknown Rado numbers corresponding to these equations. We prove new general bounds on Rado numbers inspired by the satisfying assignments discovered by the SAT solver. Our proofs require extensive case-based analyses that are difficult to check for correctness by hand, so we automate checking the correctness of our proofs via an approach which makes use of a new tool we developed with support for operations on symbolically-defined sets -- e.g., unions or intersections of sets of the form where is a symbolic variable and is a function possibly dependent on . No computer algebra system that we are aware of currently has sufficiently capable support for symbolic sets, leading us to develop a tool supporting symbolic sets using the Python symbolic computation library SymPy coupled with the Satisfiability Modulo Theories solver Z3.
Paper Structure (38 sections, 14 theorems, 24 equations, 2 tables)

This paper contains 38 sections, 14 theorems, 24 equations, 2 tables.

Table of Contents

  1. Introduction
  2. Combinatorial context
  3. Our contributions
  4. Computational Results
  5. The satisfiability (SAT) problem
  6. Encoding Rado numbers as SAT problems
  7. Variables:
  8. At least one colour is assigned to every integer:
  9. At most one colour is assigned to every integer:
  10. There is no monochromatic solution to ${\cal E}$:
  11. Breaking permutation symmetry of colours:
  12. Efficient generation of integer solutions
  13. SAT solvers and computation resources
  14. Some new exact values of $R_3({\cal E}(3,0;a,b,b))$
  15. Some new exact values of $R_3({\cal E}(3,0;a,a,b))$
  16. ...and 23 more sections

Key Result

Theorem 1.1

For nonzero integers $a_1$, $a_2$, $\dotsc$, $a_m$ and integer $c$, let $s=\sum_{i=1}^ma_i$. Then:

Theorems & Definitions (32)

  • Theorem 1.1: Rado rado1933
  • Theorem 1.2
  • Theorem 1.3
  • Theorem 1.4
  • Conjecture 1.1
  • Conjecture 1.2
  • Lemma 2.1
  • Conjecture 2.1
  • Proposition 2.1
  • proof
  • ...and 22 more