使用約束程式設計解決數學定理 | 作者：顏喬治 | 2025年1月

案例研究：準群存在問題

有些數學定理可以透過組合探索來解決。在這篇文章中，我們專注於某些準群的存在問題。我們將使用 NuCS 來展示某些準群的存在或不存在。NuCS 是一個用 Python 完全編寫的快速約束求解器，目前我正在開發它作為一個副項目，並根據 MIT 許可證發布。

讓我們開始定義一些有用的詞彙。

群

引用維基百科：

在數學中，群是一組具有運算的集合，這個運算將集合中的每一對元素關聯到集合中的一個元素（就像每個二元運算一樣），並滿足以下約束：運算是結合的，存在單位元素，且集合中的每個元素都有逆元素。

整數集合（正數和負數）與加法一起形成一個群。有許多種類的群，例如魔方的操作。

拉丁方

拉丁方是一個 n × n 的陣列，填滿 n 個不同的符號，每個符號在每一行和每一列中恰好出現一次。

一個 3×3 的拉丁方的例子是：

例如，數獨是一個 9×9 的拉丁方，並具有額外的特性。

準群

一個階數為 m 的準群是一個大小為 m 的拉丁方。也就是說，一個 m×m 的乘法表（我們將用 ∗ 表示乘法符號），其中每個元素在每一行和每一列中出現一次。

乘法法則不必是結合的。如果是，那麼準群就是一個群。

在這篇文章的其餘部分，我們將專注於某些特定準群的存在問題。我們感興趣的準群是冪等的，也就是說對於每個元素 a，有 a∗a=a。

此外，它們還具有額外的特性：

QG3.m 問題是階數為 m 的準群，其中 (a∗b)∗(b∗a)=a。QG4.m 問題是階數為 m 的準群，其中 (b∗a)∗(a∗b)=a。QG5.m 問題是階數為 m 的準群，其中 ((b∗a)∗b)∗b=a。QG6.m 問題是階數為 m 的準群，其中 (a∗b)∗b=a∗(a∗b)。QG7.m 問題是階數為 m 的準群，其中 (b∗a)∗b=a∗(b∗a)。

接下來，對於一個階數為 m 的準群，我們用 0, …, m-1 表示準群的值（我們希望這些值與乘法表中的索引相匹配）。

拉丁方模型

我們將通過利用拉丁方問題來建模準群問題。前者有兩種形式：

拉丁方問題，拉丁方 RC 問題。

拉丁方問題簡單地說，乘法表中所有行和列的值必須不同：

self.add_propagators([(self.row(i), ALG_ALLDIFFERENT, []) for i in range(self.n)])self.add_propagators([(self.column(j), ALG_ALLDIFFERENT, []) for j in range(self.n)])

這個模型為每一行 i 和每一列 j 定義了單元格的值 color(i, j)。我們稱之為顏色模型。對稱地，我們可以定義：

對於每一行 i 和顏色 c，列 column(i, c)：我們稱之為列模型，對於每個顏色 c 和列 j，行 row(c, j)：我們稱之為行模型。

注意，我們有以下特性：

row(c, j) = i <=> color(i, j) = c

對於給定的列 j，row(., j) 和 color(., j) 是逆排列。

row(c, j) = i <=> column(i, c) = j

對於給定的顏色 c，row(c, .) 和 column(., c) 是逆排列。

color(i, j) = c <=> column(i, c) = j

對於給定的行 i，color(i, .) 和 column(i, .) 是逆排列。

這正是拉丁方 RC 問題所實現的，並借助 ALG_PERMUTATION_AUX 傳播器（注意，在我之前關於旅行推銷員問題的文章中也使用了這個傳播器的較不優化版本）：

def __init__(self, n: int):super().__init__(list(range(n))) # 顏色模型self.add_variables([(0, n – 1)] * n**2) # 行模型self.add_variables([(0, n – 1)] * n**2) # 列模型self.add_propagators([(self.row(i, M_ROW), ALG_ALLDIFFERENT, []) for i in range(self.n)])self.add_propagators([(self.column(j, M_ROW), ALG_ALLDIFFERENT, []) for j in range(self.n)])self.add_propagators([(self.row(i, M_COLUMN), ALG_ALLDIFFERENT, []) for i in range(self.n)])self.add_propagators([(self.column(j, M_COLUMN), ALG_ALLDIFFERENT, []) for j in range(self.n)])# row[c,j]=i <=> color[i,j]=cfor j in range(n):self.add_propagator(([*self.column(j, M_COLOR), *self.column(j, M_ROW)], ALG_PERMUTATION_AUX, []))# row[c,j]=i <=> column[i,c]=jfor c in range(n):self.add_propagator(([*self.row(c, M_ROW), *self.column(c, M_COLUMN)], ALG_PERMUTATION_AUX, []))# color[i,j]=c <=> column[i,c]=jfor i in range(n):self.add_propagator(([*self.row(i, M_COLOR), *self.row(i, M_COLUMN)], ALG_PERMUTATION_AUX, []))

準群模型

現在我們需要為準群實現我們的額外特性。

冪等性簡單地通過以下方式實現：

for model in [M_COLOR, M_ROW, M_COLUMN]:for i in range(n):self.shr_domains_lst[self.cell(i, i, model)] = [i, i]

現在讓我們專注於 QG5.m。我們需要實現 ((b∗a)∗b)∗b=a：

這轉換為：color(color(color(j, i), j), j) = i，或等價地：row(i, j) = color(color(j, i), j)。

最後的表達式表示 j 列的 color(j,i) 元素是 row(i, j)。為了強制執行這一點，我們可以利用 ALG_ELEMENT_LIV 傳播器（或更專門的 ALG_ELEMENT_LIV_ALLDIFFERENT，優化以考慮行和列包含的元素都是不同的）。

for i in range(n):for j in range(n):if j != i:self.add_propagator(([*self.column(j), self.cell(j, i), self.cell(i, j, M_ROW)],ALG_ELEMENT_LIV_ALLDIFFERENT,[],))

同樣，我們可以建模問題 QG3.m、QG4.m、QG6.m、QG7.m。

注意，這個問題非常困難，因為搜索空間的大小是 mᵐᵐ。對於 m=10，這是 1e+100。

以下實驗是在運行 Python 3.13、Numpy 2.1.3、Numba 0.61.0rc2 和 NuCS 4.6.0 的 MacBook Pro M2 上進行的。注意，NuCS 的最新版本相對於舊版本來說速度更快，因為 Python、Numpy 和 Numba 都已升級。

以下存在/不存在的證明在不到一秒的時間內獲得：