prolog - SAT求解器序言中的基数约束

Question

我必须解决一个SAT问题。该问题有 2 个基数约束，第一个是：每天最多 6 个“同一阶段的班级”，“大学”每天“开放”12 小时，因此您必须生成约束以将它们应用于 SAT 求解器。

第二个基数约束是：每个受试者每周必须至少有 X 小时。

我一直在阅读，第一个最好的方法可能是“排序网络算法”，我不知道第二个虽然我不知道如何实现，甚至都没有开始在 prolog 中实现它。