有限全序域上约束描述问题的高效算法

### 有限全序域上约束描述问题的高效算法 #### 1. 研究背景与目的 从代数角度研究有限有序域上可处理约束的某些方面，促使我们更深入地研究有限全序域上的约束描述问题。我们旨在推广Dechter和Pearl的工作，基于Hébrard和Zanuttini更高效的布尔描述问题算法，同时补充Hähnle等人在多值逻辑方面的工作，为有限全序域上约束满足问题的完整复杂度分类奠定基础。 #### 2. 预备知识 - **基本定义**：设$D$是有限全序域，如$D = \{0, \ldots, n - 1\}$，$V$是变量集。对于$x \in V$和$d \in D$，不等式$x \geq d$和$x \leq d$分别称为正文字和负文字。约束集定义如下：逻辑常量false和true是约束；文字是约束；若$\phi$和$\psi$是约束，则$(\phi \land \psi)$和$(\phi \lor \psi)$是约束。 - **简写符号**： - $x > d$表示$x \geq d + 1$（$d \in \{0, \ldots, n - 2\}$），否则为false。 - $x < d$表示$x \leq d - 1$（$d \in \{1, \ldots, n - 1\}$），否则为false。 - $x = d$表示$x \geq d \land x \leq d$。 - $\neg false$和$\neg true$分别表示true和false。 - $\neg (x \geq d)$、$\neg (x \leq d)$、$\neg (x > d)$和$\neg (x < d)$分别表示$x < d$、$x > d$、$x \leq d$和$x \geq d$。 - $\neg (x = d)$和$x \neq d$都表示$x < d \lor x > d$。 - $\neg (\phi \land \psi)$和$\neg (\phi \lor \psi)$分别表示$\neg \phi \lor \neg \psi$和$\neg \phi \land \neg \psi$。 - **子句类型**： - 子句是文字的析取。 - 霍恩子句：最多包含一个正文字。 - 对偶霍恩子句：最多包含一个负文字。 - 双析取子句：最多包含两个文字。 - 仿射子句：$a_1x_1 + \cdots + a_{\ell}x_{\ell} = b \pmod{n}$，其中$x_1, \ldots, x_{\ell} \in V$，$a_1, \ldots, a_{\ell}, b \in D$。 - **合取范式（CNF）**：约束是合取范式，如果它是子句的合取。根据子句类型，可分为霍恩约束、对偶霍恩约束、双析取约束或仿射约束。 - **模型与满足关系**：约束$\phi(x_1, \ldots, x_{\ell})$的模型是一个映射$m: \{x_1, \ldots, x_{\ell}\} \to D$，将域元素$m(x)$分配给每个变量$x$。满足关系$m \vDash \phi$归纳定义如下： - $m \vDash true$且$m \not\vDash false$。 - $m \vDash x \leq d$如果$m(x) \leq d$，$m \vDash x \geq d$如果$m(x) \geq d$。 - $m \vDash \phi \land \psi$如果$m \vDash \phi$且$m \vDash \psi$。 - $m \vDash \phi \lor \psi$如果$m \vDash \phi$或$m \vDash \psi$。 - 仿射子句$a_1m(x_1) + \cdots + a_{\ell}m(x_{\ell}) = b \pmod{n}$被模型$m$满足。 - 满足$\phi$的所有模型的集合记为$Sol(\phi)$。 - **向量运算**：设向量$m, m', m'' \in D^{\ell}$，定义如下运算： - $m \land m' = (\min(m[1], m'[1]), \ldots, \min(m[\ell], m'[\ell]))$ - $m \lor m' = (\max(m[1], m'[1]), \ldots, \max(m[\ell], m'[\ell]))$ - $m + m' = (m[1] + m'[1] \pmod{|D|}, \ldots, m[\ell] + m'[\ell] \pmod{|D|})$ - $med(m, m', m'') = (med(m[1], m'[1], m''[1]), \ldots, med(m[\ell], m'[\ell], m''[\ell]))$ - 三元中值运算符定义为：对于$a, b, c \in D$且$a \leq b \leq c$，$med(a, b, c) = b$，也可定义为$med(a, b, c) = \min(\max(a, b), \max(b, c), \max(c, a))$。 - **向量集类型**： - 霍恩集：在合取运算下封闭。 - 对偶霍恩集：在析取运算下封闭。 - 双析取集：在中值运算下封闭。 - 仿射集：仿射空间的笛卡尔积。 #### 3. 合取范式约束 - **问题描述**：输入是有限全序域$D$上的有限向量集$M \subseteq D^{\ell}$，输出是$D$上的CNF约束$\phi(x_1, \ldots, x_{\ell})$，使得$Sol(\phi) = M$。 - **传统方法问题**：传统方法先计算补集$\overline{M} = D^{\ell} \setminus M$，为每个缺失向量$\overline{m} \in \overline{M}$构造子句$c(\overline{m})$，使得$\overline{m}$是唯一使$c(\overline{m})$为假的向量，然后将这些子句合取得到$\phi$。但该算法本质上是指数级的，因为补集$\overline{M}$可能比原向量集$M$大指数倍。 - **新算法步骤**： 1. 将集合$M$排列成有序树$T_M$，分支对应$M$中的向量。若$M$包含所有可能向量，$T_M$是分支因子为$|D|$、深度为$\ell$的完全树；否则，树中存在缺失分支，形成间隙。 2. 用文字的合取刻画这些间隙，它们的析取给出所有缺失向量的完