A Bounded Capacity Generalization of the Classic n-Queens Problem

[LucDuponcheelAtGitHub]

What is the conjecture

We introduce a generalization of the classic $n$-queens problem, parameterized by a capacity bound $0 \le c \le n$. The puzzle requires placing exactly $n . c$ coins on an $n \times n$ board such that no row, column, or diagonal contains more than $c$ coins. When $c=1$, this reduces precisely to the canonical $n$-queens formulation. We formulate this problem mathematically and present extensive empirical evidence verifying the conjecture up to $n = 1500$. Using a highly optimized local search framework based on the min-conflicts heuristic, we observe smooth polynomial execution scaling and a structural transition from highly geometric permutation-like arrangements at low $c$ to maximum-entropy, uniform distribution profiles (``noisy TV screen'') in the dense middle-spectrum where $c \approx n/2$. This smooth behavior strongly suggests that the solution space remains dense and free of hard phase transitions across all valid parameter ranges.

AMS categories

ams-05

Choose either option

• I plan on adding this conjecture to the repository
• This issue is up for grabs: I would like to see this conjecture added by somebody else

Lean code

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Fin.Basic

namespace DuponcheelConjecture

variable {n : ℕ} (hn : n ≥ 4) {c : ℕ} (hc : c ≤ n)

abbrev BoolBoard (n : ℕ) := Matrix (Fin n) (Fin n) Bool

abbrev NatBoard (n : ℕ) := Matrix (Fin n) (Fin n) ℕ

theorem n_c_coins_placement_conjecture :
    ∃ (B : BoolBoard n),
      let N := B.map (fun b ↦ if b then 1 else 0) ;
      -- Each row, column, upward diagonal, and downward diagonal
      -- contains at most `c` coins.
      ∀ i : Fin n, ∑ j : Fin n, N i j ≤ c ∧
      ∀ j : Fin n, ∑ i : Fin n, N i j ≤ c ∧
      ∀ k : ℕ, ∑ i : Fin n, ∑ j : Fin n, (if i + j = k then N i j else 0) ≤ c ∧
      ∀ k : ℤ, ∑ i : Fin n, ∑ j : Fin n, (if i - j = k then N i j else 0) ≤ c ∧
      -- Total number of coins placed is `n * c`.
      ∑ i : Fin n, ∑ j : Fin n, N i j = n * c

  := by sorry

end DuponcheelConjecture

[LucDuponcheelAtGitHub]

For your convenience I also add Lean code to experiment with. It is slower than my corresponding Haskell code. Feel free to ask for that Haskell code as well, but since this repository is mainly Lean based, I do not add the Haskell code yet.

import Std
import Init.System.IO
open Std

abbrev Row := Nat
abbrev Column := Nat
abbrev Position := Row × Column
abbrev Board := HashSet Position
abbrev Size := Nat
abbrev Count := Nat
abbrev Allowed := Nat
abbrev Conflicts := Nat
abbrev ColumnCounts := HashMap Column Count
abbrev UpDiagonalCounts := HashMap Int Count
abbrev DownDiagonalCounts := HashMap Int Count

structure BoardData where
  board : Board
  columnCounts : ColumnCounts
  upDiagonalCounts : UpDiagonalCounts
  downDiagonalCounts : DownDiagonalCounts
  size : Size
  allowed : Allowed
  conflicts : Conflicts
  boardsUntil : List BoardData
deriving Repr

partial def swapInList {α} (firstIndex secondIndex : Nat) (as : List α) : List α :=
  if firstIndex == secondIndex then
    as
  else
    match as.splitAt firstIndex with
    | (begin, rest) =>
      match rest with
      | [] => as
      | first :: after =>
        match after.splitAt (secondIndex - (firstIndex + 1)) with
        | (middle, second :: tail) =>
          begin ++ [second] ++ middle ++ [first] ++ tail
        | _ => as

@[inline] def hmFindD {α} [BEq α] [Hashable α] (m : HashMap α Nat) (k : α) : Nat :=
  m.getD k 0

@[inline] def insertCount {α} [BEq α] [Hashable α] (m : HashMap α Nat) (k : α) : HashMap α Nat :=
  let v := m.getD k 0
  m.insert k (v + 1)

@[inline] def deleteCount {α} [BEq α] [Hashable α] (m : HashMap α Nat) (k : α) : HashMap α Nat :=
  let v := m.getD k 0
  if v <= 1 then
    m.erase k
  else
    m.insert k (v - 1)

@[inline] def insertionAt (row : Row) (column : Column) (boardData : BoardData) : BoardData :=
  let position : Position := (row, column)
  { boardData with
    board := boardData.board.insert position,
    columnCounts := insertCount boardData.columnCounts column,
    upDiagonalCounts := insertCount boardData.upDiagonalCounts (Int.ofNat row - Int.ofNat column),
    downDiagonalCounts := insertCount boardData.downDiagonalCounts (Int.ofNat row + Int.ofNat column)
  }

@[inline] def deletionAt (row : Row) (column : Column) (boardData : BoardData) : BoardData :=
  let position : Position := (row, column)
  { boardData with
    board := boardData.board.erase position,
    columnCounts := deleteCount boardData.columnCounts column,
    upDiagonalCounts := deleteCount boardData.upDiagonalCounts (Int.ofNat row - Int.ofNat column),
    downDiagonalCounts := deleteCount boardData.downDiagonalCounts (Int.ofNat row + Int.ofNat column)
  }

@[inline] def conflictsAt (pos : Position) (boardData : BoardData) : Nat :=
  let row := pos.fst
  let column := pos.snd
  let allowedCount := boardData.allowed
  let the (count : Nat) := if count > allowedCount then count - allowedCount else 0
  the (hmFindD boardData.columnCounts column)
    + the (hmFindD boardData.upDiagonalCounts (Int.ofNat row - Int.ofNat column))
    + the (hmFindD boardData.downDiagonalCounts (Int.ofNat row + Int.ofNat column))

@[inline] def conflictsOn (boardData : BoardData) : Nat :=
  let f {α} (acc : Nat) (kv : α × Nat) : Nat :=
    let count := kv.2
    acc + if count > boardData.allowed then count - boardData.allowed else 0
  let columnCount := boardData.columnCounts.toList.foldl f 0
  let upDiagonalCount := boardData.upDiagonalCounts.toList.foldl f 0
  let downDiagonalCount := boardData.downDiagonalCounts.toList.foldl f 0
  columnCount + upDiagonalCount + downDiagonalCount

@[inline] def hasNoConflictsOn (boardData : BoardData) : Bool := conflictsOn boardData == 0
@[inline] def hasConflictsOn (boardData : BoardData) : Bool := conflictsOn boardData > 0

@[inline] def movementAt (row fromColumn toColumn : Column) (boardData : BoardData) : BoardData :=
  let boardData' := insertionAt row toColumn (deletionAt row fromColumn boardData)
  { boardData' with
    conflicts := conflictsOn boardData',
    boardsUntil := boardData.boardsUntil ++ [boardData']
  }

partial def toColumnsOf (fromColumns : List Column) (minConflicts : Nat) (toColumns : List Column) (row fromColumn : Column) (fromBoardData : BoardData) : List Column :=
  let rec toColumnsOf' (fromColumns' : List Column) (minConflicts' : Nat) (remaining : List Column) : List Column :=
    match remaining with
    | [] => fromColumns'
    | toColumn :: rest =>
      let movedBoardData := movementAt row fromColumn toColumn fromBoardData
      let conflicts' := conflictsAt (row, toColumn) movedBoardData
      if conflicts' < minConflicts' then
        toColumnsOf' [toColumn] conflicts' rest
      else if conflicts' == minConflicts' then
        toColumnsOf' (toColumn :: fromColumns') minConflicts' rest
      else
        toColumnsOf' fromColumns' minConflicts' rest
  toColumnsOf' fromColumns minConflicts toColumns

partial def listGet? {α} : List α → Nat → Option α
  | [], _ => none
  | x :: _, 0 => some x
  | _ :: xs, i + 1 => listGet? xs i

partial def randomElementIn {α} (as : List α) : IO α :=
  match as with
  | [] => panic! "randomElementIn: empty list"
  | _ => do
    let randomIndex ← IO.rand 0 (as.length - 1)
    match listGet? as randomIndex with
    | some x => pure x
    | none => panic! "randomElementIn: invalid index"

partial def randomShuffleOf {α} (as : List α) : IO (List α) :=
  let len := as.length
  let indices := if len == 0 then [] else List.range (len - 1)
  indices.foldlM
    (fun as' index => do
      let randomIndex ← IO.rand index (len - 1)
      pure (swapInList index randomIndex as'))
    as

partial def randomMinConflictMoveInRandomRow (fromBoardData : BoardData) : IO BoardData := do
  let rows := List.range fromBoardData.size
  let columns := List.range fromBoardData.size
  let randomRow ← randomElementIn rows
  let occupiedColumnsInRandomRow :=
    columns.filter fun column => (randomRow, column) ∈ fromBoardData.board
  let unoccupiedColumnsInRandomRow :=
    columns.filter fun column => not ((randomRow, column) ∈ fromBoardData.board)
  let randomIndex ← randomElementIn (List.range occupiedColumnsInRandomRow.length)
  let randomColumn :=
    match listGet? occupiedColumnsInRandomRow randomIndex with
    | some x => x
    | none => panic! "occupiedColumnsInRandomRow"
  let randomConflicts := conflictsAt (randomRow, randomColumn) fromBoardData
  let randomToColumns :=
    toColumnsOf [randomColumn] randomConflicts unoccupiedColumnsInRandomRow randomRow randomColumn fromBoardData
  let randomIndex2 ← randomElementIn (List.range randomToColumns.length)
  let randomToColumn :=
    match listGet? randomToColumns randomIndex2 with
    | some x => x
    | none => panic! "randomToColumns"
  if randomToColumn == randomColumn then
    pure fromBoardData
  else
    pure (movementAt randomRow randomColumn randomToColumn fromBoardData)

partial def randomBeginBoardData (n c : Nat) : IO BoardData := do
  let indices := List.range n
  let init : BoardData := {
    board := (∅ : HashSet Position),
    columnCounts := {},
    upDiagonalCounts := {},
    downDiagonalCounts := {},
    size := n,
    allowed := c,
    conflicts := 0,
    boardsUntil := []
  }
  indices.foldlM
    (fun boardData row => do
      let columns ← randomShuffleOf indices
      pure ((columns.take c).foldr (fun column bd => insertionAt row column bd) boardData))
    init

partial def untilM {α} (a2bool : α → Bool) (a2iob : α → IO α) (a : α) : IO α := do
  if a2bool a then
    pure a
  else
    let a' ← a2iob a
    untilM a2bool a2iob a'

partial def randomEndBoardData (n c : Nat) : IO BoardData := do
  let boardData ← randomBeginBoardData n c
  untilM hasNoConflictsOn randomMinConflictMoveInRandomRow boardData

def getLine : IO String := do
  let stdin ← IO.getStdin
  stdin.getLine

def printPreviousConflictsOf (boardData : BoardData) : IO Unit := do
  if boardData.conflicts != 0 then
    IO.println ("\x1b[34m " ++ toString boardData.conflicts ++ "\x1b[0m")

def showRow (n : Nat) (boardData : BoardData) (row : Nat) : String :=
  let columns := List.range n
  (columns.map fun column =>
      let position : Position := (row, column)
      if position ∈ boardData.board then
        "\x1b[31m 1\x1b[0m"
      else
        "\x1b[32m 0\x1b[0m").foldl (· ++ ·) ""

def printBoardWithPreviousConflictsOf (boardData : BoardData) : IO Unit := do
  let n := boardData.size
  printPreviousConflictsOf boardData
  for row in List.range n do
    IO.println (showRow n boardData row)

-- def ioEndBoardData (n c : Nat) : IO BoardData :=
--   randomEndBoardData n c

-- def testLarge : IO Unit := do
--   IO.println "enter a value for n: "
--   let sizeInput ← getLine
--   IO.println "enter f for showing all (n, c) values that fail"
--   IO.println "enter s for showing all (n, c) values that succeed"
--   let f_or_s ← getLine
--   let n := (String.trimAscii sizeInput).toNat?.getD 0
--   let allEndBoardData ← (List.range (n + 1)).mapM fun c => randomEndBoardData n c
--   for ((_, c), endBoardData) in
--       List.zip ((List.range (n + 1)).map fun c => (n, c)) allEndBoardData do
--     if f_or_s == "f" then
--       if hasConflictsOn endBoardData then
--         IO.println s!"(n={n}, c={c})"
--       else
--         pure ()
--     else
--       if not (hasConflictsOn endBoardData) then
--         IO.println s!"(n={n}, c={c})"
--       else
--         pure ()

def testLarge : IO Unit := do
  IO.println "enter a value for n"
  let sizeInput ← getLine
  IO.println "enter a value for c"
  let maxCountInput ← getLine
  let n := (String.trimAscii sizeInput).toNat?.getD 0
  let c := (String.trimAscii maxCountInput).toNat?.getD 0
  IO.println ""
  let endBoardData ← randomEndBoardData n c
  if not (hasConflictsOn endBoardData) then
    IO.println s!"(n={n}, c={c})"
  else
    pure ()

  -- IO.println "enter a value for n: "
  -- let sizeInput ← getLine
  -- IO.println "enter f for showing all (n, c) values that fail"
  -- IO.println "enter s for showing all (n, c) values that succeed"
  -- let f_or_s ← getLine
  -- let n := (String.trimAscii sizeInput).toNat?.getD 0
  -- let allEndBoardData ← (List.range (n + 1)).mapM fun c => randomEndBoardData n c
  -- for ((_, c), endBoardData) in
  --     List.zip ((List.range (n + 1)).map fun c => (n, c)) allEndBoardData do
  --   if f_or_s == "f" then
  --     if hasConflictsOn endBoardData then
  --       IO.println s!"(n={n}, c={c})"
  --     else
  --       pure ()
  --   else
  --     if not (hasConflictsOn endBoardData) then
  --       IO.println s!"(n={n}, c={c})"
  --     else
  --       pure ()

partial def showSmall : IO Unit := do
  IO.println "enter a value for n"
  let sizeInput ← getLine
  IO.println "enter a value for c"
  let maxCountInput ← getLine
  let n := (String.trimAscii sizeInput).toNat?.getD 0
  let c := (String.trimAscii maxCountInput).toNat?.getD 0
  IO.println ""
  let endBoardData ← randomEndBoardData n c
  IO.println "boards with conflicts counts until end board"
  IO.println ""
  for prev in endBoardData.boardsUntil do
    printBoardWithPreviousConflictsOf prev
    IO.println ""

def main : IO Unit := do
  IO.println "enter L for testing relatively large (n, c) values, say n <= 100"
  IO.println "enter S for showing relatively small (n, c) values, say n <= 20"
  let choice ← getLine
  if (String.trimAscii choice) == "L" then
    do
      IO.println "you have chosen to test large n values"
      testLarge
  else if (String.trimAscii choice) == "S" then
    IO.println "you have chosen to show small n values"
    showSmall
  else
    IO.println choice
    IO.println "you have not made a valid choice, exiting"
    pure ()

[LucDuponcheelAtGitHub]

In fact, it suffices to prove the conjecture for coprime $n$ and $c$, since, if not and if $g$ is their greatest common divisor, then tensor multiplying an all $1$ matrix of size $g$ with an $n/g$ - queens solution yields a valid "structured" solution.

[LucDuponcheelAtGitHub]

I decided to go for a pull request (#4178)