一、魔法序列问题

• 问题：对于序列 $S_0, \cdots, S_n$，如果 $\forall k$，数字 $k$ 在序列 $\{ S_i \}$ 中出现了 $S_k$ 次，那么称序列 $\{ S_i \}$ 是魔法序列。比如 5 长的 2,1,2,0,0 是一个魔法序列，因为序列中有 2 个 0，1 个 1，2 个 2，0 个 3 和 0 个 4。

  

• 显然这个问题有些 self-referential。

• 一个简单的模型是：

  int n = 5;
  range D = 0..(n-1);
  var int s[D] in D;
  solve {
  	forall (k in D) {
  		s[k] = sum((s[i]=k) for i in D)
  	}
  }
  

  • 这里用到了一个叫做 reification 的技术，是将某个约束条件转换为 0/1 变量，如果约束是 true ，变量具有 1 值、否则具有 0 值。本质上是这样的：

    var{int} b[D, D] in 0..1;
    
    solve {
    	forall (k in D) {
    		forall (i in D)
    			b[k, i] = (s[i] = k);
    		s[k] = sum(b[k, i] for i in D);
    	}
    }
    

  • 所有的条件实际上等价于：

    s[0] = (s[0]=0) + (s[1]=0) + (s[2]=0) + (s[3]=0) + (s[4]=0)
    s[1] = (s[0]=1) + (s[1]=1) + (s[2]=1) + (s[3]=1) + (s[4]=1)
    s[2] = (s[0]=2) + (s[1]=2) + (s[2]=2) + (s[3]=2) + (s[4]=2)
    s[3] = (s[0]=3) + (s[1]=3) + (s[2]=3) + (s[3]=3) + (s[4]=3)
    s[4] = (s[0]=4) + (s[1]=4) + (s[2]=4) + (s[3]=4) + (s[4]=4)
    

  • 假设我们选取了 s[0]=1：

    • 那么就有：

         1 = 0 + (s[1]=0) + (s[2]=0) + (s[3]=0) + (s[4]=0)
      s[1] = 1 + (s[1]=1) + (s[2]=1) + (s[3]=1) + (s[4]=1)
      s[2] = 0 + (s[1]=2) + (s[2]=2) + (s[3]=2) + (s[4]=2)
      s[3] = 0 + (s[1]=3) + (s[2]=3) + (s[3]=3) + (s[4]=3)
      s[4] = 0 + (s[1]=4) + (s[2]=4) + (s[3]=4) + (s[4]=4)
      

    • 就有 s[1] ≥ 1，就有 s[1]=0 不成立，第一行变为：

      1 = 0 + 0 + (s[2]=0) + (s[3]=0) + (s[4]=0)
      

二、Stable Marriages

• 问题：有 $N$ 位男生和 $N$ 位女生。每个男生都对所有女生有一个喜欢程度的排名 $R_B[n]$，每个女生也对所有男生有一个喜欢程度的排名 $R_G[n]$。请配对 $N$ 对男女生，使得他们的关系都是「稳定的」，一对稳定关系的男生 $B_0$ 和女生 $G_0$ 的定义如下：

  • 如果有其他女生（记为 $G_1$）在 $B_0$ 的排名中比 $B_0$ 现在的配偶 $G_0$ 更高，$B_0$ 在 $G_1$ 的排名中一定要比 $G_1$ 现在的配偶（记为 $B_1$）要更低，否则说 $B_0$ 和 $G_1$ 可能会抛弃 $G_0$ 和 $B_1$ 而私奔；
  • 如果有其他男生（记为 $B_1$）在 $G_0$ 的排名中比 $G_0$ 现在的配偶 $B_0$ 更高，$G_0$ 在 $B_1$ 的排名中一定要比 $B_1$ 现在的配偶（记为 $G_1$）要更低，否则说 $G_0$ 和 $B_1$ 可能会抛弃 $B_0$ 和 $G_1$ 而私奔。

• 建模：

  • 命名部分：我们做成这个样子

    enum Boys = { George, Hugh, Will, Clive };
    enum Girls = { Julia, Halle, Angelina, Keira };
    
    int rank_boys[Boys, Girls]; # 表示男孩给出的对女孩的排序位次
    int rank_girls[Girls, Boys]; # 表示女孩给出的对男孩的排序位次
    
    var{Girls} wife[Boy];
    var{Boys} husband[Girls];
    

  • 约束部分：保证任意两对不会私奔

    solve {
    
    	# 保证关系一致性
    	forall (b in Boys)
    		husband[wife[b]] = b;
    	forall (g in Girls)
    		wife[husband[g]] = g;
    	
    	# 保证任意一对 b, g 组合不会发生私奔
    	forall (b in Boys, g in Girls)
    		# 对 g 而言，如果更喜欢 b，要保证 b 更不喜欢 g
    		rank_boys[b, g] < rank_boys[b, wife[b]] => rank_girls[g, b] > rank_girls[g, husband[g]]
    		# 对 b 而言，如果更喜欢 g，要保证 g 更不喜欢 b
    		rank_girls[g, b] < rank_girls[g, husband[g]] => rank_boys[b, g] > rank_boys[b, wife[b]]ssss
    }
    

• 其中的重要思路：

  • Indexing：将列表或矩阵的结果作为 Index 嵌套起来。
  • Logical combination：逻辑组合。

• 简化方法：

  • 留意到我们只需要保证不发生私奔，我们可以假设

  • 留意到 $p \to q$ 本质上等价于 $\neg p \vee q$。因而可以对原始形式作如下等值演算：

    • $(b_< \to g_>) \wedge (g_< \to b_>)$：原始形式。
    • $(\neg b_< \vee g_>) \wedge (\neg g_< \vee b_>)$：等值演算。
    • $(b_\ge \vee g_>) \wedge (g_\ge \vee b_>)$： 将不等号的取反整进去。
    • $(b_\ge \wedge g_\ge) \vee (b_> \wedge g_>) \vee (b_\ge \wedge b_>) \vee (g_\ge \wedge g_>)$：分配律。
    • $((b_> \vee b_=) \wedge (g_> \vee g_=)) \vee (b_> \wedge g_>) \vee ((b_> \vee b_=) \wedge b_>) \vee ((g_> \vee g_=) \wedge g_>)$：拆开不等号。
    • $((b_> \vee b_=) \wedge (g_> \vee g_=)) \vee (b_> \wedge g_>) \vee b_> \vee g_>$：最后两项使用吸收律 $A \wedge (A \vee B) \Leftrightarrow A$。
    • $((b_> \vee b_=) \wedge (g_> \vee g_=)) \vee b_> \vee g_>$：再用吸收律 $A \vee (A \wedge B) \Leftrightarrow A$。
    • $(b_> \wedge g_>) \vee (b_> \wedge g_=) \vee (b_= \wedge g_>) \vee (b_= \wedge g_=) \vee b_> \vee g_>$：再次拆分。
    • $(b_= \wedge g_=) \vee b_> \vee g_>$：再用分配律。

  • 因而可以写成：

    # 保证任意一对 b, g 组合不会发生私奔
    forall (b in Boys, g in Girls)
    	(rank_boys[b, g] = rank_boys[b, wife[b]] AND rank_girls[g, b] = rank_girls[g, husband[g]]) OR rank_boys[b, g] > rank_boys[b, wife[b]] OR rank_girls[g, b] > rank_girls[g, husband[g]] 
    

三、数组映射相关的传播方法

• 一个简单的例子是：

  range DX = {0, 1, 2, 3, 4, 5};
  var{int} x in DX;
  
  range DY = {3, 4, 5};
  var{int} y in DY;
  
  DY arr[DX] = [0:3, 1:4, 2:5, 3:5, 4:4, 5:3];
  
  solve
  {
  	y = c[x];
  }
  

  • 假如了解到 y \\neq 3，那么就能相应的根据 y = c[x] 约束去划掉 x=0 和 x=5 的可能。
  • 但请注意，如果了解到 x \\neq 4，并不能直接划掉 y=4，因为还有 1:4 这个映射。但如果还给出 x \\neq 1，就能断定 y \\neq 4。