💻 computer science

Compact SAT and MaxSAT Encodings for Business-to-Business Meeting Scheduling with Idle-Time Balancing

本文介绍了一种用于 B2B 会议调度的紧凑型 SAT 和 MaxSAT 编码，该编码利用领域过滤和共享变量来显著减少子句数量和内存使用量，同时最小化参与者的空闲时间范围，在求解效率方面优于已发表的 MaxSAT 公式以及商业求解器 Gurobi。

原作者： Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

发布于 2026-08-04

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你是一位顶级派对策划师，正在筹备一场规模宏大、高规格的商业大会。你有数百人需要进行一对一会议，但每个人的时间表都各不相同，有些房间很小，而有些则非常宽敞，而且某些会议必须在其他会议开始之前完成。你的目标不仅仅是让每个人都开成会，还要确保没有人会在预约之间等待太久而感到无聊。这就是“业务对业务（B2B）会议调度”这一复杂的逻辑谜题。

为了解决这个问题，计算机科学家使用了一种特殊的逻辑游戏，叫做 SAT（可满足性问题）。把 SAT 想象成一个超级聪明的侦探，它会检查一组规则是否能同时成立。如果你告诉侦探：“会议 A 必须在会议 B 之前，但会议 B 又必须在会议 A 之前”，侦探会立刻说：“不可能！”但如果规则虽然复杂却又是合理的，侦探就能找到一个有效的调度方案。另一种版本 MaxSAT 则更进一步，它不仅是一个寻找有效方案的侦达，还会试图通过最小化人们等待的时间来让方案变得“完美”。这篇论文深入探讨了我们如何让这些逻辑侦探在组织这些复杂的商务活动时变得更快、更聪明。

问题所在：错综复杂的会议网

在商业会议的世界里，事情很快就会变得混乱。你有一份会议清单、一份时间段清单和一份房间清单。规则是严格的：

无重叠： 一个人不能同时出现在两个地方。
房间限制： 房间容纳的会议数量不能超过其容量。
先后顺序： 某些会议必须发生在其他会议之前（比如上午的简报会要在下午的工作坊之前）。
“闲置”问题： 真正的头痛在于“闲置时间”。如果一名参与者在上午 9:00 有一个会议，而下一个会议要到 11:00 才开始，那么他们就有两小时的“闲置时间”。这项研究的目标是平衡这一点，确保不会出现有人等了好几个小时，而其他人只等了几分钟的情况。这关乎公平与效率。

旧方法 vs. 新方法

研究人员观察了一种现有的方法（称为 ORG-MAXSAT），该方法已经相当出色。然而，他们注意到这种方法就像是通过写下宾客和时间的每一个可能组合来组织派对，甚至包括那些显而易见的无效组合。这导致它臃肿、缓慢且消耗大量计算机内存。

来自越南理工大学（VNU）的研究团队决定构建一个“紧凑版”。他们引入了三个主要技巧来缩小问题规模：

“预检”过滤器（领域过滤）： 在向计算机侦探提问之前，他们添加了一个智能过滤器。这个过滤器会查看规则并立即剔除不可能的选项。例如，如果一个会议必须在下午 2:00 结束的另一个会议之后进行，过滤器会立即从可能的选项列表中移除下午 2:00 之前的任何时间段。这就像是在试图找一支特定的笔之前，先清理掉桌上的杂物。他们证明了这个过滤器永远不会丢弃有效的解；它只剔除了垃圾信息。
“共享阶梯”（稀疏共享后缀编码）： 在处理“必须在……之前”的规则时，旧方法会为每一对会议都写一条单独的笔记。如果你有 100 个会议，就会产生数千条笔记。新方法注意到许多笔记表达的是相同的内容。与其分别写下“会议 A 在 B 之前”、“会议 A 在 C 之前”和“会议 A 在 D 之前”，不如创建一个共享的逻辑“阶梯”。他们复用了相似情况下的变量，就像是用一把万能钥匙打开多扇门，而不是为每一把锁都制作一把新钥匙。
“公平性”评分（闲置时间平衡）： 他们没有仅仅计算人们有多少次休息，而是创建了一种衡量“闲置时间”的新方法。他们观察了每个人从“第一次会议”到“最后一次会议”之间的时间跨度。如果某人的会议在 9:00 和 11:00，那么他们的“跨度”就是两小时。如果他们只有一个会议，则闲置时间为零。目标是使“最忙碌的人的闲置时间”与“最不忙碌的人的闲置时间”之间的差异尽可能小。

研究发现

研究人员使用他们的“紧凑型”方法与旧方法以及一些非常强大的商业软件（如 Gurobi 和 CPLEX）进行了对比，测试了 126 个官方测试用例和 100 个包含更多会议的额外“压力测试”用例。

以下是令人印象深刻的结果：

体积更小： 新方法平均减少了 40.3% 的逻辑“子句”（即计算机需要检查的规则）。
内存占用更低： 它节省了 55.9% 的峰值内存。想象一下，只需要一半的 RAM 就能解决同样的谜题。
速度更快： 解决问题的总时间下降了 14.0%。
过滤器的力量： 单独使用“预检”过滤器就减少了 24.1% 的变量和 16.2% 的规则。
共享的力量： “共享阶梯”技巧根据日程的拥挤程度，又削减了 0.5% 到 5.5% 的规则。

结论

最令人兴奋的部分是，他们的新型紧凑型 SAT 和 MaxSAT 方法能够解决所有 126 个官方测试用例。更棒的是，在处理中位数时间方面，它比领先的商业求解器 Gurobi 还要快。虽然其他商业工具（如 CPLEX 和 CP Optimizer）在规定时间内难以解决所有案例，但这种新的基于 SAT 的方法成功处理了所有案例。

这篇论文并不声称已经解决了宇宙中所有的调度问题，但它确实证明了通过清理规则和更聪明地分配工作，我们可以让计算机更好地组织我们的繁忙生活。它将一个巨大的、纠缠不清的会议乱麻，变成了一个整洁、平衡的进度表，让每个人都能获得公平的时间，而不必在走廊里长时间等待。

技术摘要：用于平衡空闲时间的紧凑型 SAT 与 MaxSAT 编码（针对 B2B 会议调度问题）

问题定义

本文研究了 B2B（企业对企业）会议调度，这是一个组合优化问题，要求将请求的成对会议分配到特定的时间槽和地点。调度必须满足以下约束：

参与者不重叠： 参与者不能同时参加两个会议。
地点容量： 任何时间槽内的会议数量不得超过可用地点数 ( $K$ )。
可用性与限制： 会议必须在请求的会话、固定时段或禁止时段内进行。
前序关系： 有向弧 $(i, j)$ 强制要求会议 $i$ 必须在会议 $j$ 之前发生。

本研究提出的目标函数不同于以往的公式化方法（以往通常最小化“休息组”或限制休息次数的差异）。相反，本研究旨在最小化具有至少两次会议的参与者之间内部空闲槽总数的极差 ( $\Delta I$ )。内部空闲槽被定义为参与者第一次和最后一次分配会议之间的非占用时间。该指标能够区分短时间中断与长时间等待，旨在实现类似于平衡学术课程问题（BACP）的负载均衡分布。文中还报告了总空闲时间 ( $I_\Sigma$ ) 作为补充指标。

方法论

作者提出了一种紧凑的 SAT（布尔可满足性）和 MaxSAT 编码，该编码集成了相对于现有已发表公式的三项主要建模改进：

保持解的领域过滤（预处理）：
在生成合取范式（CNF）之前，作者应用了一个预处理算法（算法 1）来移除不支持的赋值。这集成了：
- 端点边界过滤器： 沿路径传播前序约束（使用直接弧或传递闭包）。
- 逐参与者匹配： 移除对于特定参与者而言无法构成无冲突日程的赋值。
- 饱和槽传播： 消除已被强制赋值占满容量的槽位。
- 声称： 该过程在保留所有可行解的同时减少了领域规模，从而减少了变量和子句的数量。
稀疏共享后缀前序编码 (SPARSESUFFIX)：
作者没有使用两两配对的子句来编码前序关系（这在领域规模较大时可能呈二次方增长），而是引入了一种稀疏编码。
- 它仅实例化前序领域中约束变得活跃的独特“切点”。
- 它复用了不同关系中相同的辅助变量。
- 该方法被证明与两两配对的子句等价，但显著减少了子句数量，尤其是在结合领域缩减时。
基于范围的空闲时间目标：
论文引入了一种精确编码来最小化内部空闲槽的极差 ( $\Delta I$ )。
- 它推导出每个参与者的第一个和最后一个占用槽位。
- 它使用线性数量的辅助变量来计算所有相关参与者之间最大和最小空闲计数之差。

研究通过将这些组件与基准 ORG-MAXSAT 公式（一种对已发表模型的改编）以及商业求解器（Gurobi、CPLEX、CP Optimizer）进行对比评估。评估涵盖了 126 个官方基准实例和 100 个具有不同前序密度生成的“压力测试”实例。

核心贡献

本文确定了三个具体的贡献：

预处理程序： 一种在 CNF 生成前移除不支持赋值的过滤器集成。命题 1 证明了该过程保持了可行性，实验结果显示它减少了 24.1% 的赋值变量和 16.2% 的子句。
稀疏共享后缀表示： 一种精确编码 (SPARSESUFFIX)，仅实例化所需的的前序领域切点。命题 3 证明了其与两两配对子句的等效性。研究表明，虽然领域缩减降低了变量数量，但后缀共享独立地降低了子句数量。
B2B 特有的目标： 一种基于范围的空闲时间目标，用于衡量内部等待时间的差异，并使用线性数量的辅助变量进行编码。

实验结果

实验在 4 核机器上进行，时间限制为 7,200 秒。主要发现包括：

公式规模与内存： 与改编后的 ORG-MAXSAT 基准相比，所提出的紧凑编码将中值子句数量减少了 40.3%，并将中值峰值内存使用量减少了 55.9%。
领域缩减的影响： 仅领域过滤就减少了 24.1% 的赋值变量和 16.2% 的子句，是公式规模缩减的最大贡献者。
前序编码： SPARSESUFFIX 编码在官方前序实例上减少了 0.5%–1.0% 的中值子句数量，并在结合传递闭包后的最高密度派生实例上减少了高达 5.5%。
求解器性能：
- 所有三种提出的 SAT/MaxSAT 方法（增量式 SAT、非增量式 SAT 和 UWrMaxSAT）都解决了全部 126 个官方实例。
- 与 Gurobi（唯一解决所有实例的商业求解器）相比，所提出的 SAT/MaxSAT 方法实现了更低的中值总时间。
- 增量式 SAT 在所有完整方法中实现了最低的中值时间 (0.227s)。
- CP Optimizer 具有最低的中值时间 (0.110s)，但在时间限制内未能解决 11 个实例。

意义与主张

本文声称，所提出的紧凑编码为 B2B 会议调度提供了比现有布尔公式更显著的效率提升。通过将领域过滤与前序表示分离，作者证明了领域缩减是减少公式规模的主要驱动力，而稀疏共享后缀编码则在独立于关系集的情况下提供了额外的子句削减。

研究断言，新的空闲时间范围目标提供了一种比以往“休息组”指标更细致的调度质量衡量标准，能够区分短时间中断与长时间等待。此外，结果表明，配备这些紧凑编码的现代 SAT 和 MaxSAT 求解器，在处理此类特定问题时，其求解速度的中值可以优于领先的商业 MIP 和 CP 求解器，并在某些商业求解器超时的情况下解决了所有基准实例。

作者对未来的工作保持谦逊，指出当前研究侧重于单次运行计时，未来的研究可以探索重复计时运行以及词典序目标（在最小化 $\Delta I$ 之前先最小化 $I_\Sigma$ ）。