1/40
Solving and Verifying the Boolean Pythagorean
Triples Problem
3/40
Introduction
4/40
Schur’s Theorem [Schur 1917]
Can the set of natural numbers {1, 2, . . . } be partitioned into
k parts with no part containing a, b, and c such that a+b=c?
Otherwise, what is the smallest finite counter-example?
4/40
Schur’s Theorem [Schur 1917]
Can the set of natural numbers {1, 2, . . . } be partitioned into
k parts with no part containing a, b, and c such that a+b=c?
Otherwise, what is the smallest finite counter-example?
{1} →
{1} →
{1, 4} →
{1, 4} → × {} {2} {2} {2, 3}
init 1+1=2 2+2=4 1+3=4 1+4=5
2+3=5
4/40
Schur’s Theorem [Schur 1917]
Can the set of natural numbers {1, 2, . . . } be partitioned into
k parts with no part containing a, b, and c such that a+b=c?
Otherwise, what is the smallest finite counter-example?
{1} →
{1} →
{1, 4} →
{1, 4} → × {} {2} {2} {2, 3}
init 1+1=2 2+2=4 1+3=4 1+4=5
2+3=5
Theorem (Schur’s Theorem)
For each k > 0, there exists a number S(k), known as Schur
number k, such that [1, S(k)] can be partitioned into k parts
with no part containing a, b, and c such that a + b = c, while
this is impossible for [1, S(k)+1].
S(1) = 1, S(2) = 4, S(3) = 13, S(4) = 44 [Baumert 1965],
160 ≤ S(5) ≤ 315 [Exoo 1994, Fredricksen 1979].
5/40
Schur’s Theorem on Squares
Can the set of squares {1
2
, 2
2
, 3
2
, . . . } be partitioned into k
parts with no part containing a, b, and c such that a + b = c?
5/40
Schur’s Theorem on Squares
Can the set of squares {1
2
, 2
2
, 3
2
, . . . } be partitioned into k
parts with no part containing a, b, and c such that a + b = c?
The case k = 2 is already very difficult to determine:
A Small SAT Problem: Pythagorean Triples up to n = 55
(x3 ∨ x4 ∨ x5) ∧ (¯x3 ∨ x¯4 ∨ x¯5) ∧ (x5 ∨ x12∨x13) ∧ (¯x5 ∨ x¯12∨x¯13) ∧
(x7 ∨ x24∨x25) ∧ (¯x7 ∨ x¯24∨x¯25) ∧ (x9 ∨ x40∨x41) ∧ (¯x9 ∨ x¯40∨x¯41) ∧
(x6 ∨ x8 ∨ x10) ∧ (¯x6 ∨ x¯8 ∨ x¯10) ∧ (x8 ∨ x15∨x17) ∧ (¯x8 ∨ x¯15∨x¯17) ∧
(x10∨x24∨x26) ∧ (¯x10∨x¯24∨x¯26) ∧ (x12∨x35∨x37) ∧ (¯x12∨x¯35∨x¯37) ∧
(x14∨x48∨x50) ∧ (¯x14∨x¯48∨x¯50) ∧ (x9 ∨ x12∨x15) ∧ (¯x9 ∨ x¯12∨x¯15) ∧
(x15∨x36∨x39) ∧ (¯x15∨x¯36∨x¯39) ∧ (x12∨x16∨x20) ∧ (¯x12∨x¯16∨x¯20) ∧
(x16∨x30∨x34) ∧ (¯x16∨x¯30∨x¯34) ∧ (x20∨x48∨x52) ∧ (¯x20∨x¯48∨x¯52) ∧
(x15∨x20∨x25) ∧ (¯x15∨x¯20∨x¯25) ∧ (x18∨x24∨x30) ∧ (¯x18∨x¯24∨x¯30) ∧
(x24∨x45∨x51) ∧ (¯x24∨x¯45∨x¯51) ∧ (x21∨x28∨x35) ∧ (¯x21∨x¯28∨x¯35) ∧
(x20∨x21∨x29) ∧ (¯x20∨x¯21∨x¯29) ∧ (x24∨x32∨x40) ∧ (¯x24∨x¯32∨x¯40) ∧
(x28∨x45∨x53) ∧ (¯x28∨x¯45∨x¯53) ∧ (x27∨x36∨x45) ∧ (¯x27∨x¯36∨x¯45) ∧
(x30∨x40∨x50) ∧ (¯x30∨x¯40∨x¯50) ∧ (x33∨x44∨x55) ∧ (¯x33∨x¯44∨x¯55)
(x3 ∨ x4 ∨ x5) ∧ (x¯3 ∨ x¯4 ∨ x¯5) ∧ (x5 ∨ x12∨x13) ∧ (x¯5 ∨ x¯12∨x¯13) ∧
(x7 ∨ x24∨x25) ∧ (x¯7 ∨ x¯24∨x¯25) ∧ (x9 ∨ x40∨x41) ∧ (x¯9 ∨ x¯40∨x¯41) ∧
(x6 ∨ x8 ∨ x10) ∧ (¯x6 ∨ x¯8 ∨ x¯10) ∧ (x8 ∨ x15∨x17) ∧ (x¯8 ∨ x¯15∨x¯17) ∧
(x10∨x24∨x26) ∧ (x¯10∨x¯24∨x¯26) ∧ (x12∨x35∨x37) ∧ (x¯12∨x¯35∨x¯37) ∧
(x14∨x48∨x50) ∧ (x¯14∨x¯48∨x¯50) ∧ (x9 ∨ x12∨x15) ∧ (x¯9 ∨ x¯12∨x¯15) ∧
(x15∨x36∨x39) ∧ (¯x15∨x¯36∨x¯39) ∧ (x12∨x16∨x20) ∧ (x¯12∨x¯16∨x¯20) ∧
(x16∨x30∨x34) ∧ (¯x16∨x¯30∨x¯34) ∧ (x20∨x48∨x52) ∧ (x¯20∨x¯48∨x¯52) ∧
(x15∨x20∨x25) ∧ (¯x15∨x¯20∨x¯25) ∧ (x18∨x24∨x30) ∧ (x¯18∨x¯24∨x¯30) ∧
(x24∨x45∨x51) ∧ (¯x24∨x¯45∨x¯51) ∧ (x21∨x28∨x35) ∧ (¯x21∨x¯28∨x¯35) ∧
(x20∨x21∨x29) ∧ (x¯20∨x¯21∨x¯29) ∧ (x24∨x32∨x40) ∧ (¯x24∨x¯32∨x¯40) ∧
(x28∨x45∨x53) ∧ (x¯28∨x¯45∨x¯53) ∧ (x27∨x36∨x45) ∧ (¯x27∨x¯36∨x¯45) ∧
(x30∨x40∨x50) ∧ (x¯30∨x¯40∨x¯50) ∧ (x33∨x44∨x55) ∧ (x¯33∨x¯44∨x¯55)
