Constructing strong starters of orders $3p$: triplication with SAT solver

This paper presents a novel "triplication" algorithm that constructs strong starters of order $3p$from those of order$p$ by reducing the problem to a Sudoku-type constraint satisfaction task solved efficiently using the z3 SAT solver, thereby offering a practical approach to investigating Horton's conjecture.

The Gist

Here is an explanation of the paper using simple language, creative analogies, and metaphors.

The Big Picture: Building a Giant Puzzle from a Small One

Imagine you are a master puzzle maker. You have a small, perfect puzzle piece (a Strong Starter) that fits together perfectly. Now, you want to build a massive, complex puzzle that is exactly three times bigger than the original.

The problem? You can't just copy the small piece three times; the math gets messy, and the pieces won't fit. For decades, mathematicians have wondered: Is it always possible to build this "triple-sized" puzzle?

This paper says: Yes, we can! But we need a special recipe called "Triplication."

---

The Ingredients: The Base and the Key

To start, you need two things:

1. The Base Starter: A small, perfect puzzle (let's say size 7).
2. The Key: A secret number (like a password) that helps unlock the expansion.

Think of the Base Starter as a blueprint for a small house. The Key is the specific type of brick you decide to use to expand it.

The Magic Trick: The "Triplication Table"

The authors invented a method to take that small house blueprint and stretch it into a 3-column table.

• Column 1: The original blueprint.
• Column 2: The blueprint shifted by your "Key."
• Column 3: The blueprint flipped and shifted.

When you lay these three columns side-by-side, you get a giant grid. But here's the catch: The numbers in this grid are currently in a "foreign language" (modulo 7). To make the giant puzzle work, we need to translate these numbers into a new, simpler language: Modulo 3 (which only uses the numbers 0, 1, and 2).

The Challenge: The "Modular Sudoku"

This is where the paper gets exciting. We need to fill in the missing numbers (0, 1, or 2) in our giant grid so that:

• Every row has unique differences.
• Every row has unique sums.
• No two numbers in the same "color group" are the same.

The authors call this a "Modular Sudoku." It's like a Sudoku puzzle, but instead of a 9x9 grid, it's a long, skinny grid with very specific, tricky rules.

The Analogy:
Imagine you are a spy (like "Cindy" in the paper's story) trying to decode a message.

• The Base Starter is the original message.
• The Triplication Table is the encrypted code.
• The Modular Sudoku is the cipher key you need to crack.
• If you can solve the Sudoku, you can unlock the secret to building the giant puzzle. If you can't, the giant puzzle doesn't exist (or at least, not using this method).

The Computer's Role: The "SAT Solver"

Solving this Sudoku by hand is incredibly hard, like trying to find a needle in a haystack while wearing blindfolded gloves.

So, the authors used a SAT Solver (specifically a tool called z3).

• What is a SAT Solver? Think of it as a super-fast, hyper-logical robot that never gets tired. It tries millions of combinations of 0s, 1s, and 2s in a split second to see if a valid solution exists.
• The Result: The robot found solutions for many different sizes of puzzles, proving that the "Triplication" method works for many cases where mathematicians weren't sure before.

Why Does This Matter? (The Horton Conjecture)

There is a famous guess in math called Horton's Conjecture. It says: "You can always build these strong starters for any odd number, unless the number is 3, 5, or 9."

For a long time, nobody knew if this was true for numbers divisible by 3 (like 21, 33, 39). This paper provides a construction kit. It shows how to build them.

• Before: "We think they exist, but we can't build them."
• After: "Here is the blueprint and the robot that builds them. If the robot finds a solution to the Sudoku, the puzzle exists!"

The Catch and the Future

The paper admits that the robot (SAT solver) is a bit slow for very large puzzles. It's like using a sledgehammer to crack a nut—it works, but it's heavy.

• The Good News: The robot proved the method works for many cases.
• The Next Step: The authors plan to build a specialized tool (a custom algorithm) that will be much faster and smarter than the general robot.

Summary in a Nutshell

1. The Goal: Build a giant math puzzle (size $3p$) from a small one (size$p$).
2. The Method: Use a "Triplication" recipe to create a grid.
3. The Hurdle: Fill the grid with 0s, 1s, and 2s following strict rules (a "Modular Sudoku").
4. The Solution: Use a computer robot (SAT solver) to solve the Sudoku.
5. The Victory: If the robot solves it, you have successfully built a new, giant Strong Starter, proving that these mathematical structures exist in many more places than we thought.

It's a story of taking a small, known truth and using logic and computers to expand it into a much larger, previously unknown world.

Technical Summary

Here is a detailed technical summary of the paper "Constructing strong starters of orders 3p: triplication with SAT solver."

1. Problem Statement

The paper addresses the construction of strong starters in cyclic groups of order $n = 3p$, where $p$ is an odd integer coprime to 3.

• Definition: A strong starter in a cyclic group $Z_n$ (where $n$ is odd) is a partition of the non-zero elements $\{1, \dots, n-1\}$ into pairs $\{a_i, b_i\}$ such that:
  1. All pair sums $a_i + b_i$ are distinct and non-zero modulo $n$.
  2. All pair differences $\pm(a_i - b_i)$ are distinct and non-zero modulo $n$.
• Context: While strong starters are known to exist for most odd orders, their existence for orders divisible by 3 (specifically $n=3p$) is not fully theoretically settled. Horton's conjecture (1989) suggests they exist for all such orders except $n=3$ and $n=9$, but this remains unproven for large $n$.
• Gap: Existing theoretical results guarantee existence only for small $n$ or specific conditions. There is a lack of constructive methods for $n=3p$ when $p$ is large and coprime to 3.

2. Methodology: The Triplication Algorithm

The authors propose a novel constructive method called triplication, which builds a strong starter of order $3p$from a known strong starter of order$p$. The process reduces the combinatorial problem to a Constraint Satisfaction Problem (CSP) modulo 3, described as a "modular Sudoku" problem.

Step 1: The Base and Key

• Input: A strong starter $T$ of order $p$ (where $\gcd(p, 3)=1$) and a "key" integer $t \in \{0, \dots, p-1\}$.
• Constraint: The key $t$ must not be 0 and must not be equal to any pair sum in the base starter $T$ (i.e., $t \notin \hat{T} \cup \{0\}$).

Step 2: Constructing the Triplication Table ($\Sigma_p$)

The method constructs a table $\Sigma_p$ with $3q+1$rows (where$q=(p-1)/2$) and 3 columns:

1. Top Row: Contains the pair $(t, t)$.
2. Column 1: The base starter $T = [(x_i, y_i)]$.
3. Column 2: The shifted starter $T^+_t = [(t+x_i, t+y_i)] \pmod p$.
4. Column 3: The reflected/shifted starter $T^-_t = [(t-y_i, t-x_i)] \pmod p$.

This table defines a set of pairs modulo $p$. To form a starter of order $3p$, these pairs must be lifted to integers modulo$3p$ using the Chinese Remainder Theorem (CRT). This requires determining the values of these pairs modulo 3.

Step 3: The Modular Sudoku Problem ($\Sigma_3$)

The core of the method is finding a table $\Sigma_3$ of pairs $(U_i, V_i)$ modulo 3 that satisfies specific constraints derived from the structure of $\Sigma_p$:

1. Row Constraints: In every regular row (rows 1 to $q$), the differences $D_i = U_i - V_i \pmod 3$ must be distinct (i.e., $\{0, 1, 2\}$).
2. Weak Set Constraints: Pairs in $\Sigma_p$ that share the same sum modulo $p$ (called "weak sets") must have distinct sums modulo 3. If the sum modulo $p$ is 0, the sum modulo 3 must be non-zero.
3. Color (Monochrome) Constraints: For any value $c$ appearing in $\Sigma_p$, the positions where $c$ appears must map to distinct values modulo 3 in $\Sigma_3$. (Note: The value 0 appears twice in $\Sigma_p$; a dummy variable is used to enforce distinctness).

Step 4: Reconstruction

If a valid solution for $\Sigma_3$ exists, the final strong starter $S$ of order $3p$is constructed by combining the values from$\Sigma_p$(mod$p$) and$\Sigma_3$ (mod 3) via CRT:
$$a_i \equiv u_i \pmod p, \quad a_i \equiv U_i \pmod 3$$
$$b_i \equiv v_i \pmod p, \quad b_i \equiv V_i \pmod 3$$

3. Key Theoretical Contributions

• Theorem 1 (Correctness): Proves that if a solution to the modular Sudoku problem exists for a given base starter $T$ and key $t$, the resulting set $S$ is a valid strong starter of order $3p$.
• Theorem 2 (Necessary Condition): Establishes that if the key $t$ is 0 or equal to any pair sum in $T$, the Sudoku problem has no solution. This provides a quick filter for invalid parameters.
• Theorem 3 (Symmetry): Proves that solutions come in pairs. If $\{U_i, V_i\}$ is a solution, then swapping values 1 and 2 (applying the automorphism $x \to -x \pmod 3$) yields another valid solution.
• Inverse Problem Algorithm: The authors provide a sufficient condition (an algorithmic test) to determine if a given strong starter of order $3p$was *not* generated by triplication, based on the row structure of its reduction modulo$p$.

4. Experimental Results

The authors implemented the method using the Z3 SAT solver (Microsoft) in Python.

• Performance:
  • Small Orders ($p < 100$): The solver finds solutions very quickly (e.g., $p=7$ takes ~0.06s; $p=97$ takes ~90s). The execution time roughly follows a heuristic $O(m^2 \ln m)$.
  • **Medium Orders ($100 < p < 500$):** Execution times increase significantly but remain tractable (e.g.,$p=499$ takes ~18,000s). The growth is non-monotonic, suggesting sensitivity to the specific structure of the base starter and the chosen key.
  • Comparison: Directly searching for a strong starter of order 39 using a SAT solver took ~200 seconds. Using triplication (finding a starter of order 13 and solving the Sudoku) took <1 second.
• Success Rate: In all tested cases where the necessary condition (Theorem 2) was met, a solution was found, supporting a conjecture that a solution always exists for valid inputs.
• Randomness: The distribution of solution times varies significantly based on the specific key $t$ chosen, even for the same base starter.

5. Significance and Implications

• Constructive Proof: The method provides a practical way to generate strong starters for orders $3p$ where theoretical existence proofs are lacking, effectively extending the known range of existence.
• Efficiency: The triplication approach is significantly more efficient than direct SAT solving or hill-climbing algorithms for large orders divisible by 3. It decomposes a hard problem of size $3p$into a smaller problem of size$p$plus a modular CSP of size$3p$.
• New Research Object: The "modular Sudoku" problem is identified as a new combinatorial object. While the authors used a general-purpose SAT solver, they note that a specialized algorithm for this specific constraint structure could be even faster.
• Limitations: The method relies on the existence of a base strong starter of order $p$. While starters exist for all odd $p$, finding strong starters for specific $p$ can still be computationally intensive, though easier than for $3p$.

In summary, the paper bridges a gap in combinatorial design theory by offering a robust, algorithmic framework (triplication) to construct strong starters for orders divisible by 3, validated by extensive computational experiments using SAT solvers.