对合金 4.2 使用地形排序

Question

我正在尝试使用拓扑排序来找到两个不同的顺序调度，它们遵循它们的先决条件。当我执行代码时，没有找到任何实例，我不知道为什么。这是我的代码：

open util/relation

abstract sig Course {
    prereq: set Course, -- c->d in prereq if c is a prerequisite of d
    s1, s2: set Course      -- two sequential course schedules
}
one sig cs1121, cs1122, cs1141, cs2311, cs2321,
                cs3000, cs3141, cs3311, cs3331, cs3411, cs3421, cs3425 extends Course { }

fact {
    no prereq.cs1121
    prereq.cs1122 = cs1121
    prereq.cs1141 = cs1122
    prereq.cs2311 = cs1121
    prereq.cs2321 = cs1122
    prereq.cs3000 = cs3141
    prereq.cs3141 = cs2311
    prereq.cs3141 = cs2321
    prereq.cs3311 = cs2311
    prereq.cs3331 = cs1141
    prereq.cs3331 = cs2311
    prereq.cs3331 = cs2321
    prereq.cs3411 = cs1141
    prereq.cs3411 = cs3421
    prereq.cs3421 = cs1122
    prereq.cs3425 = cs2311 
    prereq.cs3425 = cs2321
}

-- is the given schedule a topological sort of the prereq relation?
pred topoSort [schedule: Course->Course] {
    (all c: Course | lone c.schedule and lone schedule.c) -- no branching in the schedule
    and totalOrder[*schedule, Course] -- and it's a total order
    and prereq in ^schedule -- and it obeys the prerequisite graph
}


pred show {
    s1.irreflexive  and s2.irreflexive  -- no retaking courses!
    s1.topoSort and s2.topoSort -- both schedules are topological sorts of the prereq relation
    s1 != s2    -- the schedules are different
}

run show

Answer 1

将求解器（在选项菜单下）切换到 MiniSAT with Unsat Core，然后查看内核。你会看到它突出显示

 prereq.cs3141 = cs2311
 prereq.cs3141 = cs2321

这与您的无分支规则相矛盾。