AI 中文总结
本文针对企业对企业会议调度问题，提出兼顾空闲时间平衡的紧凑SAT与MaxSAT编码，实验表明其在子句数量、内存使用及求解效率上均优于已有方法与商用求解器Gurobi。
AI 中文摘要
企业对企业会议调度需在可用性、容量、冲突及优先级约束下，将请求的成对会议分配至时间槽与地点。已发表的布尔公式会保留传播可消除的会议-时间槽分配，并以成对子句编码优先级关系。本文提出基于保解域过滤、选定优先级边界共享变量及最小化参与者内部空闲时间总量范围目标的紧凑SAT与MaxSAT编码。针对126个官方实例及100个更高密度衍生实例开展实验，检验域过滤、优先级表示、传递关系及优化方法。与采用相同目标的适配版已发表MaxSAT公式相比，所提编码将中位数子句数减少40.3%，中位数峰值内存使用量减少55.9%；仅域过滤就将分配变量减少24.1%、子句减少16.2%；选定优先级边界共享变量在官方优先级实例上减少子句0.5%-1.0%，在最高衍生密度下最多减少5.5%。空闲时间度量可区分单槽中断与更长等待，总空闲时间则提供互补度量。与领先商用求解器Gurobi相比，三种SAT与MaxSAT方法均以更低中位数总时间求解所有官方实例。
英文摘要
Business-to-business meeting scheduling assigns requested pairwise meetings to time slots and locations under availability, capacity, conflict, and precedence constraints. The published Boolean formulation retains meeting-slot assignments that propagation can eliminate and encodes precedence relations with pairwise clauses. We present compact SAT and MaxSAT encodings based on solution-preserving domain filtering, variables shared at selected precedence boundaries, and an objective that minimizes the range of participants' internal idle-slot totals. Experiments on 126 official and 100 higher-density derived instances examine domain filtering, precedence representation, transitive relations, and optimization method. Compared with an adapted published MaxSAT formulation using the same objective, the proposed encoding reduces the median clause count by 40.3% and median peak memory usage by 55.9%. Domain filtering alone reduces assignment variables by 24.1% and clauses by 16.2%. Sharing variables at selected precedence boundaries reduces clauses by 0.5%-1.0% on official precedence instances and by up to 5.5% at the highest derived density. The idle-time measure distinguishes one-slot interruptions from longer waits, while aggregate idle time provides a complementary measure. Compared with Gurobi, a leading commercial solver, all three SAT and MaxSAT methods solve every official instance with lower median total times.
