在权力与逻辑之间寻求平衡：基于精确可满足性的、兼顾能源效率的装配线设计方法

《Computers & Operations Research》：Balancing power with logic: Exact satisfiability-based methods for energy-aware assembly lines

　　摘要
简单装配线平衡问题（SALBP）是生产和制造领域中的一个基本优化挑战。在本文中，我们探讨了一个新近引入的变体——带有电力峰值最小化的简单装配线平衡问题（SALB3PM），该问题的目标是降低电力消耗峰值。尽管这一问题受到了越来越多的关注，但现有的方法尚未充分利用基于逻辑的方法的潜力。本研究提出了基于满足性（SAT）和最大满足性（MaxSAT）公式化的精确求解方法，以高效解决SALB3PM问题。在一组来自文献的300个实例上进行了一项实验研究，使用了包括SAT、MaxSAT、整数线性规划（ILP）、约束编程（CP）和伪布尔优化（PBO）在内的多种范式的最先进求解器。结果清楚地表明，所提出的基于满足性的方法优于整数线性规划方法。从这个意义上说，本文介绍的策略为扩展到其他SALBP变体提供了有希望的视角。

引言
简单装配线是一种高效的制造系统，由一系列按顺序排列的工作站组成，并通常通过传送带连接（Scholl, 1999）。产品的生产过程被定义为一系列具有固定处理时间和优先关系的任务，即一个任务只有在所有前置任务完成后才能被处理。简单装配线平衡问题（SALBP）包括将任务分配给工作站，以满足优先约束并优化指定的目标函数。每个工作站一次最多只能处理一个任务，并且必须在固定的周期时间内完成所有分配的任务。图1展示了一个简单装配线平衡的例子。单个产品通过一系列连续的工作站进行处理，每个工作站都在固定的周期时间内执行其分配的任务。在任何给定的周期时间内，不同的产品同时在不同的工作站上被处理；因此，系统在不同工作站之间并行运作。SALBP被认为是NP难的（Scholl, 1999），并且有许多变体，它们主要在目标函数上有所不同。例如，SALBP-1旨在最小化给定周期时间??的工作站数量，而SALBP-2则旨在最小化给定工作站数量??的周期时间。关于SALBP变体的详细综述可以在Boysen等人（2007, 2022）的文献中找到。
在本文中，我们专注于带有电力峰值最小化的简单装配线平衡问题（SALB3PM）（Gianessi等人，2019），这是一个新近引入的SALBP变体，其中加入了能源驱动的优化标准。在这个变体中，工作站的数量??和周期时间??都是固定的，每个任务??都与一个恒定的电力消耗????相关联。目标是最小化电力峰值，即在周期时间内观察到的最大总电力消耗。通过引入电力峰值的视角，SALB3PM从而弥合了可行SALBP解决方案与环保制造系统之间的差距。根据Gahm等人（2016）的研究，尽管能源是制造系统中的关键因素，但减少能源需求对于可持续发展至关重要。此外，生产计划的峰值电力需求直接影响生产成本。例如，Artigues等人（2013）提出了一个案例研究，其中安排了金属加工操作以最小化电力成本。在这种情况下，必须避免电力峰值，以防止过高的电力费用。同样，Massoudi等人（2019）和Kemmoe等人（2017）考虑了一个情况，即能源供应合同对最大总电力需求设定了上限。超过这个合同限制可能会导致因违约而产生的财务处罚。
最近，Delorme和Gianessi（2024）将电力峰值的最小化作为可重构制造系统线路平衡的主要目标。根据作者的观点，电力消耗是由多个任务的同时处理造成的，因此取决于任务在工作站的分配及其调度。在周期化的生产线上，能源消耗模式会在每个生产周期重复出现。因此，必须在装配线设计的早期阶段就考虑能源相关因素，特别是在线路平衡过程中。

正如Gianessi等人（2019）所声称的，由于增加了电力峰值最小化的考虑，SALB3PM比SALBP更为复杂。这一目标需要在工作站内对任务进行调度决策，这为解决方案空间引入了额外的维度，并且在表示特定解决方案时需要额外的状态变量。这一因素增加了问题的组合复杂性。我们提出了基于满足性（SAT）和最大满足性（MaxSAT）公式的精确解决方法，利用了满足性求解技术的最新进展。实际上，SAT和MaxSAT作为强大的建模范式的有效性已在许多实际应用中得到了验证，这些应用涵盖了硬件和软件验证（Clarke等人，2004, Gupta等人，2006, Safarpour等人，2007）、规划和调度（Cherif等人，2024, Surynek，2019, Vasquez和Hao，2001，Xu等人，2002）、生物信息学（Gra?a等人，2010, Guerra和Lynce，2012, Lynce和Marques-Silva，2006）等多个领域。
SAT是确定给定合取范式（CNF）公式是否可满足的决策问题。MaxSAT是SAT的优化扩展。在其最一般的形式中，称为加权部分MaxSAT，输入包括一组硬条款和一组加权软条款。目标是找到一个满足所有硬条款的同时最大化满足软条款总权重的分配。我们提出了两种主要的SALB3PM解决方法：基于SAT的方法和基于MaxSAT的方法，每种方法都有不同的编码和/或搜索方案。基于SAT的方法将SALB3PM转化为一系列SAT实例，即一系列决策问题。我们使用了三种不同的方案，分别是结构感知搜索SAT-STR、二分搜索SAT-BS和SAT-UNSAT搜索SAT-SU。相比之下，基于MaxSAT的方法通过构建一个单一的加权部分MaxSAT实例来解决SALB3PM问题。我们还探索了问题目标的不同编码方式，并为SALB3PM引入了简化规则。所有提出的方法的有效性通过广泛的计算实验得到了验证。

本文扩展了我们在ICTAI 2024（Zheng等人，2024）上发表的工作，并在Pragmatics of SAT 2024研讨会（Py等人，2024）上进行了展示。在ICTAI论文中，首次引入了SALB3PM的MaxSAT模型：一个初始模型和一个带有二进制表示方案的增强模型。在研讨会论文中，提出了一种初始的基于SAT的方法。在这项工作中，我们从约束和目标建模的角度重新审视了基于满足性的公式化。本文的贡献主要有三个方面：
• 四种用于解决SALB3PM的基于满足性的方案：三种不同的基于SAT的方法，以及一种基于MaxSAT的公式化。
• 用于减小公式大小的简化规则。
• 广泛的计算实验，比较了所提出的方法与其他最先进的问题解决范式：约束编程（CP）、整数线性规划（ILP）和伪布尔编程（PB）。

本文的其余部分组织如下：第2节介绍了与SALB3PM、SAT和MaxSAT相关的基本定义和符号。第2节还回顾了相关的工作以及Gianessi等人（2019）提出的原始基于ILP的方法。第3节介绍了SALB3PM约束的基于满足性的公式化，第4节介绍了SALB3PM目标的基于满足性的公式化。第5节提出了SALB3PM的简化规则。这三节共同构成了第6节中详细描述的SAT和MaxSAT方法的公式化。第7节展示了实验结果。最后，在第8节我们进行了总结并讨论了未来的工作。

**SALB3PM**
我们现在正式介绍这个问题以及整篇论文中使用的符号。设??表示从1到??编号的??个任务集，设??={??1,??2,…,????}表示??个工作站集。每个工作站一次最多只能处理一个任务，并且必须在周期时间??内完成所有分配的任务。设??={0,1,…,???1}表示离散时间单位集。每个任务??∈??都与一个持续时间????和一个电力消耗????相关联，并且必须分配给恰好一个工作站。

**基于满足性的SALB3PM约束公式化**
在本节中，我们介绍了SALB3PM约束的基于SAT的编码。在第2.1节回顾的ILP公式化中，我们可以注意到，除了唯一的整数电力峰值变量????????之外，所有其他变量都是布尔变量，所有约束都可以容易地转换为命题子句或伪布尔约束。我们的SAT编码通过明确表示任务活动状态来扩展了ILP模型。

**基于满足性的SALB3PM目标公式化**
在本节中，我们提出了两种SALB3PM目标函数（GDM-0）的编码方式。这些编码方式补充了上一节中介绍的约束编码和下一节中介绍的简化规则，共同构成了SALB3PM的完整解决方案框架。具体来说，我们提出了两种替代表示方法：初始公式化（OBJ-I）和增强公式化（OBJ-E），这两种方法在以下两个小节中有详细描述。

**简化规则**
现在我们介绍两种简化规则，这些规则被纳入了SAT和MaxSAT公式化中：一种来自经典SALBP文献的优先级简化规则，以及一种基于SALB3PM中工作站内任务排序的长任务简化规则。需要注意的是，这些简化规则在第7节的所有计算实验中都得到了考虑。确实，简化规则在缩小搜索空间方面起着重要作用，从而加快了解决过程的速度。

**用于SALB3PM的SAT和MaxSAT方法**
在本节中，我们基于第3节的约束编码和第5节的目标函数编码，介绍了SALB3PM的SAT和MaxSAT方法。基于SAT的SALB3PM方法的本质是将优化问题分解为一系列决策子问题。这导致了不同的搜索方案，这些方案集成了SAT预言机。关于后者，考虑了不同版本的SAT预言机，即第节中介绍的结构感知SAT方法SAT-STR。

**实验结果**
本节对使用CP、ILP、PB、SAT和MaxSAT等类别的最先进求解器对各种SALB3PM公式化进行了全面的实证评估。我们首先在第7.1节详细介绍了实验协议，包括计算环境、基准数据集和求解器配置。随后，在第7.2节进行了整体性能的比较分析，重点关注每种方法在所有基准测试中的表现。

**结论和未来工作**
在这项工作中，我们提出了基于满足性的精确方法，用于简单装配线平衡并最小化电力峰值。我们提出了两种MaxSAT方法（对应于两种目标公式化）和五种SAT方法：一种基于结构的方法、两种基于SAT-UNSAT搜索的方法以及两种基于二分搜索的方法。进行了广泛的实验来评估我们提出的公式化和方法，包括与ILP、CP和伪布尔范式的比较。

**作者贡献声明**
Zhifei Zheng：写作——审稿与编辑、写作——初稿、可视化、验证、软件、方法论、调查、形式分析、数据管理、概念化。
Sami Cherif：写作——审稿与编辑、验证、监督、软件、项目管理、方法论、调查、资金获取、形式分析、概念化。
Matthieu Py：写作——审稿与编辑、验证、软件、方法论、调查、形式分析、概念化。

**致谢**
这项工作部分得到了ANR-24-CE23-6126项目（BforSAT）和ANR-19-CHIA0013-01主席职位（MASSAL’IA）的支持，该项目由法国国家研究机构和法国电力分配网络运营商Enedis共同资助。同时，我们还获得了皮卡第朱尔·凡尔纳大学“Plateforme MatriCS”的高性能计算资源，该资源得到了欧盟欧洲区域发展基金（FEDER）和上法兰西大区 Council等机构的共同资助。

**作者名单**
Zhifei Zheng | Sami Cherif | Matthieu Py | Rui S. Shibasaki | Chu-Min Li | Laurent Deroussi | Nathalie Grangeon
Laboratoire MIS, UR 4290, Université de Picardie Jules Verne, 33 rue Saint-Leu, Amiens, 80039, Cedex 1, France