约束式编程学习笔记[3] 约束求解算法实例 完全性证明框架 Term Equations及解法及证明_约束求解器公式

3 Constraint programming in a nutshell

3.3 Example: Boolean constraints

0. Q: 在 x ∈ { 0 , 1 } x ∈ { 0 } ∣ x ∈ { 1 } \frac{x\in\{0,1\}}{x\in\{0\}|x\in\{1\}} x∈{ 0}∣x∈{ 1}x∈{ 0,1}​中，如何理解“As already noted there this rule is parametrized by a variable, the choice of which is of relevance here, and by a value, the choice of which is of no relevance here. We use this rule in combination with the heuristic…”？
   A: 选取0还是选取1是对称的，但选取哪个$x$可能在实际执行中对效率产生决定性影响。根据经验，我们采用一定的启发式方法，即选择出现在最多约束中的变量。其实这和人类在进行分类讨论时的选择十分一致。
1. Q: 形式上的表达式$x\wedge y=z,z=1\to x=1,y=1$就告诉我们 ⟨ x ∧ y = z ; x ∈ D x , y ∈ D y , z ∈ { 1 } ⟩ ⟨ ; x ∈ { 1 } , y ∈ { 1 } , z ∈ { 1 } ⟩ \frac{\langle x\wedge y = z;x\in D_x,y\in D_y, z\in\{1\}\rangle}{\langle ;x\in\{1\},y\in \{1\},z\in\{1\}\rangle} ⟨;x∈{ 1},y∈{ 1},z∈{ 1}⟩⟨x∧y=z;x∈Dx​,y∈Dy​,z∈{ 1}⟩​嘛？
   A: 否，因为 D x = { 0 } D_x=\{0\} Dx​={ 0}时，上述规则将导致错误结果。（回忆我们传播约束的目的：除了找解，还有可能直接排除一些情况，直接得出一些$\perp$. 此处的传播在 D x = { 0 } D_x=\{0\} Dx​={ 0}时就能直接产生inconsistency，排除！）
2. Q: 作为人类专家，你怎么得到“six rules for the constraint $x\wedge y=z$”呢？
   A: 相当于手动搜索出决策树。
   例如：
   如果$z=1$，则直接$x=1,y=1$.
   否则讨论，若$x=1$，则$y=0$.
   否则讨论，若$y=1$，则$x=0$.
   否则，该条约束无价值。
   当然，实际设计“树”时可以利用各类技术，设法减少节点个数，使得树更平衡，等等，以提升性能。

3.4 Example: polynomial constraints on integer intervals

0. Q: 用一句话概括预处理时，书中两条transformation rule.
   A: 把复杂度高的公式拆成数个复杂度低的公式并对每个子公式换新变量名。
1. Q: 举例说明“整数区间的四则运算”(interval arithmetic)不一定得到整数区间。
   A: 比如区间乘区间显然得不到质数（233）
   再比如区间除以一个数没问题，但除以一个有$n$个整数的区间有可能得到$n$部分分立的结果。
2. Q: 如何理解$int([-3..5]/[-1..2])=\mathcal{Z}$？
   A: 首先$int(\cdot )$含义类似于“凸包”，即是区间且包含一切可能结果（当然在结果是$\mathcal{Z}$时输出就是$\mathcal{Z}$），其次注意根据interval arithmetic定义，0除以0得到一切数。
3. Q: 如何理解启发式规