多次分组，所有成员在同一组中至少会面一次

Question

我想将人们分成更小的子组，并在连续 sessions 多次洗牌后，让所有人至少见面一次。

在每个 session 中，人们被分成固定数量的组。每个session.
团体人数应最接近（人数）/（团体人数）。人数不能太少也不能太多。
session一直持续到每一对人至少见面一次。
最好尽量减少同一对情侣见面的次数。

以下是11个人（编号0-10）3组（3列）对这道题的回答。它需要 5 session 秒。

Session 1: 3,6,8,10     0,1,7,9     2,4,5
Session 2: 3,5,7,8      0,1,2,10    4,6,9
Session 3: 0,1,6,8      2,3,4,9     5,7,10
Session 4: 0,3,5,9      1,4,8,10    2,6,7
Session 5: 1,3,5,6      2,8,9,10    0,4,7

上面的问题很相似，但我更想让人们在一个更大的群体中见面，而不是一对一。

以下是我使用Alloy的方法。这适用于少数人 (~15) 和小组 (~2)，但当规模增加时，它很快会导致计算时间爆炸。我需要为 ~25 人和 ~5 组计算它。

module Teaming

sig Person { groups: some Group }

sig Group { people: some Person }

sig Session { groups: some Group }

one sig Sessions { sessions: some Session }

sig GroupPerSession {}

-- Tree structures
fact {
    all s: Session | s in Sessions.sessions
    all g: Group | g in Session.groups
    all s: Session | all p:Person | p in s.groups.people
    people =~ groups
}

-- The total number of people
fact {
    all s: Session | #s.groups.people = #Person
}

-- The number of groups per session
fact {
    all s: Session | #s.groups = #GroupPerSession
}

-- The number of people in a group
fact {
    all g: Group | (#g.people) >= div[#(Person), #(GroupPerSession)] and (#g.people) <= add[div[#Person,#GroupPerSession],1]
}

-- Mutually exclusive grouping in a session
fact separate {
    all s: Session | all disj a,b: s.groups | no p: Person | p in a.people and p in b.people
}

-- Every pair of people meets somewhere
pred sameGroup {
    all disj a,b: Person | some g: Group | a in g.people and b in g.people
}

-- The same people should not meet too many times
fact sameGroupNotTooMuch {
    all disj a,b: Person | #{a.groups & b.groups} <= 3
}

run sameGroup for 6 Int, 5 Session, 15 Group, exactly 3 GroupPerSession, exactly 16 Person
run sameGroup for 6 Int, 6 Session, 24 Group, exactly 4 GroupPerSession, exactly 18 Person
run sameGroup for 6 Int, 7 Session, 35 Group, exactly 5 GroupPerSession, exactly 18 Person

我想动态规划应该可行，但我找不到任何具体的东西。任何改进 Alloy 代码或其他算法的指针都会很棒。

Answer 1

这是我解决这个问题的快速方法。总体而言，实例的生成似乎更快，但在尝试将 >20 人分配到 >4 组时仍然难以完成。

module Teaming

one sig Settings{
    maxEncounter:Int,
    minGroupSize:Int,
    maxGroupSize:Int
}{
// Manually filling values there helps (1)reducing the integer bit-width needed (2) decrease the complexity (in terms of clauses)
  maxEncounter=4
 //minGroupSize=5
 //maxGroupSize=5
  minGroupSize=div[#Person, #Group]
  maxGroupSize=add[minGroupSize,1]
}

sig Session{}{
    Group.people[this]=Person // all person are assigned in group during a session
    no disj g1,g2 :Group| g1.people[this]  & g2.people [this] !=none // a person can't be in two disjoint groups of a same session

}

sig Group { 
    people: Session some -> some Person 
}{
   all s:Session|  #people[s]<= Settings.maxGroupSize and   #people[s]>=Settings.minGroupSize 
}

sig Person {}


pred allMeet {
    all disj a,b: Person | people. a & people.b != none->none
}

pred allMeetAndMinEncounter {
    all disj a,b: Person | let x= (people. a & people.b) {
        #x <=Settings.maxEncounter
        x != none ->none
   }
}


run allMeet for 6 Int, 9 Session, exactly 4 Group, exactly 20 Person

带来的变化亮点：

尽可能删除量化
删除了冗余约束
用三元关系代替了两个二元关系组和人。这有几个优点：
- 它将实例中存在的组原子数减少到每个会话的组总数。
- 它允许在实例查看器中使用实例投影。你现在可以分别查看每个会话的小组分配。

Answer 2

我认为 Alloy 不是优化的正确工具。它是一个专注于寻找反例的规范工具。但是，当然可以找到像这样的谜题的解法。（我认为有一个小组开发了 Alloy 的扩展，最大限度地减少了找到的解决方案。）

虽然我是初学者，但我还是试了一下。令人惊讶的是，我找到了一个包含 4 个会话、11 个人和 3 个小组的解决方案。

  s0   {2,9,10},  {5,6,7,8},  {0,1,3,4}, 
  s1   {2,4,7,8}, {1,3,6,10}, {0,5,9}, 
  s2   {1,2,3,5}, {0,7,8,10}, {4,6,9}, 
  s3   {0,2,6},   {4,5,10},   {1,3,7,8,9}

由于 Alloy 不是优化器，我使用二进制方法找到最小会话数，我发现 25/5 至少需要 7 个会话。

这是我的完整模型：

sig P, Group {}
sig Session {
  participants : Group -> P
}

fact {
  // tuning goes here (max sure <= scope )
  # Group = 5
  # P = 25
  # Session = 7

  // In every session, people are divided into a constant number 
  // of groups.
  all s : Session | s.participants.P = Group

  // The sessions are continued until every pair of people 
  // meets each other at least once.
  // Preferably, the number of times the same pair meet 
  // each other should be minimized.
  all disj a,b : P | some participants.a & participants.b

  // Everyone has to join one group in every session.
  all p : P, s : Session | one s.participants.p

  // The group size should be closest to (the number 
  // of people)/(# of groups).
  // There should not be a 
  // groups of too few people or too many people.
  all g : Group, s : Session | (# s.participants[g]) >= 3
}

run {} for 5 Group, 25 P, 24 Session, 6 int

为这些数字指定 int 宽度至关重要。

找到一系列 8 个会话用了 5 秒，找到 7 个会话用了更长的时间，34 秒。通过增加最小值来强制更平等的组大小仍然是运行 :-)

我认为该工具的功能完全符合预期：找到 a 解决方案。不太好找最优解。

多次分组，所有成员在同一组中至少会面一次

Grouping of people multiple times, where all the members meet each other in the same group at least once

dynamic-programming

combinatorics

alloy