引入子句割: 混合整数线性规划中 MaxSAT 问题的强 No-Good 割
最优化与控制
2025-09-29 v1
摘要
本文引入了子句割: 由 CNF 公式逻辑蕴含的子句导出的线性不等式, 类似于增强的 no-good 割. 利用这些割, 我们收紧了随机加权部分 MaxSAT 问题的混合整数线性规划 (MILP) 公式, 该问题对核心引导的完备 MaxSAT 求解器而言一直极具挑战性. 我们的方法将在 LP 松弛中取得整数值的变量视为部分赋值, 并将其作为假设提供给 SAT 求解器. 当出现不可行时, 这些赋值会被子句割排除, 并由 SAT 求解器进一步增强. 我们提出了两种分离算法: 一种利用 SAT 预言机在取得整数值的变量集合中寻找子句割; 另一种则在评估部分赋值时, 使用冲突驱动子句学习 (CDCL) SAT 求解器学习到的子句. 在 SATLIB 基准上的实验表明, 与通用 MILP 求解器 Gurobi 12 相比, 性能获得了高达两个数量级的显著提升, 整个问题集的运行时间仅为 Gurobi 的 7.8%. 结果也超越了专用的 MaxSAT 求解器 RC2, 运行时间仅为其 60%. 在某些情况下, 我们的优化耗时仅略长于对 SAT 公式的单次 SAT 调用. 我们解释了这些性能提升的来源以及标准 MILP 公式在此场景下的局限性.
引用
@article{arxiv.2509.21687,
title = {Introducing Clause Cuts: Strong No-Good Cuts for MaxSAT Problems in Mixed Integer Linear Programming},
author = {Max Engelhardt and Milan Adhikari and Jonasz Staszek and Alexander Martin},
journal= {arXiv preprint arXiv:2509.21687},
year = {2025}
}
备注
21 pages, 9 figures