基于最大可满足性问题的专业实验方案设计

刘燕丽　余艳　张婷

摘要：基于最大可满足性问题的专业实验方案以组合拍卖为应用背景，采用命题逻辑建模、分支限界算法，针对问题设计优化的存储结构。专业实验方案展现了一个完整的工业问题的解决过程，内容涉及程序设计语言、数据结构、离散数学、算法设计等计算机核心课程相关内容，有助于加强学生专业知识的系统化。

关键词关键词：实验教学；算法设计；数据结构；NP问题

DOIDOI：10.11907/rjdk.143639

中图分类号：TP302

文献标识码：A文章编号文章编号：16727800（2015）002003703

作者简介作者简介：刘燕丽（1980-）， 女，河南西平人，硕士，武汉科技大学理学院讲师，研究方向为NP问题的高效求解、近似算法。

0引言

目前，学生在程序设计学习过程中尚不能独立建立课程之间的横向联系，对所学专业缺乏系统、立体的认识[13]。造成这一问题的因素较多，若在教学活动中多设计可以展现计算机解决某类自然界问题的完整过程的实验方案，将有助于培养学生系统、立体、计算机程序方式的问题解决能力。基于最大可满足性问题的专业实验方案以培养学生问题解决能力和建立系统化思维模式为目标，以组合优化问题为背景，给出最大可满足性问题的求解算法设计，阐明如何利用命题逻辑对实际问题进行建模，如何选择数据存储方式以及对复杂问题内部关系进行解剖，是利用计算机解决社会活动问题的一个完整案例。

1最大可满足性问题模型优化

最大可满足性问题（Maximum Satisfiability Problem，MaxSAT）是SAT问题的一个重要扩展，是经典的NP难题。最大可满足性问题利用命题逻辑以及谓词描述绝大多数组合优化问题，具有强大的建模能力，如最大团、最少图着色数、最大割集、最小可满足性问题等均可转换为MaxSAT问题来求解。同时，该问题在工业生产和社会活动中有广泛应用，如生产调度、组合拍卖、超大规模集成电路测试、排课问题等。MaxSAT算法国际竞赛网站每年都接收来自不同领域工业问题的新算例。

1.1MaxSAT问题相关概念

设F=x1∧（x-1∨x2∨x3）∧（x-4∨x-5）。这里xi是取值为真或假的命题变元。真值指派是指命题变元取“真”或“假”的状态。符号xi及其否定形式x-i称为文字，记为li。xi称为正文字，x-i称为负文字。xi=1时，正文字为真，xi=0时，负文字为真。若干文字的析取项称为子句，如x-1∨x2∨x3。特别地，若只含有1个文字，称之为单子句，如x1。不含文字的子句是空子句，记为□。若干子句的合取构成合取范式，记为F。文字为真，称该文字满足。若子句中至少有一个文字满足，则称该子句满足，否则子句不满足。如x1=1，x2=0，x3=0子句x-1∨x2∨x3不满足，在其余7种真值指派下，该子句满足。合取范式满足是指范式中任意一个子句均被满足。

1.2实际问题转化

组合拍卖问题是现实商业活动中常见的一个组合优化问题。对于若干拍卖品，每个商家给出各自竞拍商品组合的价格。在满足一个商品只能卖给一个商家的条件下，求解卖家可获取的最大销售额。组合拍卖问题转换为MaxSAT问题求解的例子如下：设集合Goods={gi， i∈N且1≤i≤10}，表示有10件商品。Sales={[（ g1， g2， g3），101]， [（ g2， g3， g5， g6），150]， [（ g1， g7， g8），120]， [（ g4， g9， g10），100]， [（ g1， g5， g9），180]， [（ g4， g6， g10），200]}，表示6个买家购买的商品和出价。如[（ g1， g2， g3），101]表示第一个买家出价101元竞拍1、2、3号商品。求解如何出售这10个商品可以获得最大销售额。建立模型，设命题变元xi表示第i个买家出价竞拍商品事件。

xi=1，第i个买家拍卖成功xi=0，否则，拍卖失败

命题变元集合V={x1，x2，x3，x4，x5，x6}。因为同一件商品只能卖给一个买家，所以有相同商品的购买事件不能同时为真。如第一个买家和第三个买家同时购买商品g2、g3，事件x1、x3不能同时成立。因此该问题约束条件的硬子句集合为{x-1∨x-3，x-1∨x-5，x-1∨x-2，x-2∨x-5，x-2∨x-6， x-4∨x-5，x-4∨x-6}，软子句集合为{x1，x2，x3，x4，x5， x6}。每个买家的出价是相应软子句的权重。组合拍卖问题转换为V集合上，在满足所有硬子句的条件下，求解一组V集合上变元的指派，使得满足的单子句权重和最大。图1是组合拍卖所应用的模型图。无向图的结点是6个命题变元，若第i个买家和第j个买家购买的商品有冲突，则结点Si与结点Sj间有一条无向边。

至此，商品的组合拍卖问题转化为加权偏MaxSAT问题。命题逻辑的建模过程，应完成3个步骤：①设置表示某一事实的判断命题变元；②完成约束关系的描述，利用9个关系连接词建立约束条件；③利用等价转换将命题逻辑转换为最小完备集与、或、非的合取范式。

2算法设计

求解一组变元真值指派使得可满足软子句权重最大，算法需遍历2n的二叉树搜索空间。

2.1算法框架

对于含有m个文字的子句，只有当m个文字均为假时，子句不满足，因而对于子句而言不满足状态的变元真值指派较容易确定。MaxSAT算法将求解最大满足子句数等价转换为求解最小不满足子句数。采用分支限界法设计的MaxSAT完备算法，上界是当前最优的一组完整的变元真值指派确定的不满足子句数，其初始值为合取范式子句数。下界是在当前分支点，合取范式不可满足子句数的一个下界，其初始值为0。算法[4]描述如下：

算法1MaxSAT完备算法。输入：合取公式F和初始上界UB输出：F的最小不满足子句数及对应的真值指派if（F= or只包含空子句） return 空子句数；LB=在当前部分真值指派下的空子句数+下界的保守估计；if（LB≥UB）return UB；选择分支变元x；if（Maxsatz（x=0）

2.2下界保守估计计算方法

利用单子句传播测试冲突集的方法可确定不可满足的子句数。算法2描述了单子句传播的过程[56]。

算法2单子句传播。输入：单子句ci输出：空子句或简化后的F①令单子句ci中的文字l为真，单子句满足；②检查其余子句，对形如l∨li…∨lk含有文字l的子句，移除整个子句，因为该子句已满足；③对形如∨li…∨lk含有的子句，删除文字，简化子句为li…∨lk，特别地，当子句只含有一个文字时，该子句简化为空子句；④若有空子句产生或无新的单子句产生，单子句传播结束，否则，对③产生的新单子句重复以上步骤。单子句传播算法中的空子句指不含任何文字的特殊子句，通常记为□。单子句传播操作是检测不可满足子句的主要工具。单子句传播操作的执行过程如下：设F1={x1，x-1∨x2，x-1∨x6，x-1∨x4，x-4∨x-5，x5，x1∨x5，x2∨x6，x4∨x7}。子句x1的单子句传播过程是：①令x1=1，子句x1∨x5满足，移除该子句；子句x-1∨x2，x-1∨x6和x-1∨x4，分别简化为x2、x6和x4，无空子句产；②对新产生的单子句x2进行单子句传播，令x2=1，子句x2∨x6满足，无空子句产生；③对新产生的单子句x6进行单子句传播，令x6=1，无空子句产生；④对新单子句x4进行单子句传播，令x4=1，子句x-4∨x-5化简为x-5，无空子句产生。移除满足的子句x4∨x7；⑤对新单子句x-5，令x5=0，删除相反文字后，单子句x5化简为空子句。子句x1的单子句传播过程结束。为了方便分析x1的单子句传播过程，可借助推理图进行分析。推理图的原理是x-i∨xj等价于xi→xj。当xi为真时，xi→xj的值为真当且仅当xj的值为真。图2显示了x1的单子句传播过程。

图1组合拍卖模型图2单子句x1传播过程

单子句传播是广度优先的一种遍历方式。从图2的空子句出发，逆向追溯可以找到产生该空子句的原因子句是{x1，x-1∨x4，x-4∨x-5，x5}。此子句集是一个冲突集，在变元x1，x4，x5的任意一种真值指派下，冲突集中至少有1个子句是不满足的，所以一个冲突集代表一个不可满足的子句，下界的估计值加1。

2.3数据结构选择

数据结构是算法设计的一个重要实施环节，不同的数据结构对于算法效率的影响是显著的[710]。实验中数据结构的选择部分设计了两个问题：①根据程序局部性原理，如何安排子句的结构；②根据单子句传播操作过程及回溯，如何实现单子句传播。

程序局部性原理是Cache的工作原理。该原理说明程序数据的使用具有时间、空间局部性。基于此原理，在设计子句存储结构时，把单子句操作中常用的子句状态、子句长度、子句文字等存放为结构体，子句的其它信息存放为一维数组。原因是单子句传播操作是算法的核心操作，被调用得非常频繁。单子句传播每次寻找含有相反文字的子句并将该文字从子句中删除，该操作涉及到子句中的文字、子句的长度、子句的状态。为了加快子句搜索，需要建立子句索引，索引中存放包含有此文字的子句序号。建立索引的优势是加快单子句传播过程中相反文字子句的寻找。计算机通过索引可以快速确定包含文字及相反文字的子句，而无需扫描所有子句。索引的建立可以在算例输入时完成，时间代价小。

单子句传播操作是检测冲突集的主要手段，是从1个单子句出发推理出冲突子句，再通过追溯找到造成冲突的子句构成冲突集。通常，1个单子句可以构成多个冲突，但只能记为1个冲突集。程序通过广度优先方式能找到最短路径的冲突集，节省冲突集计算时间。由以上分析可知，单子句传播的数据结构应设计为栈，以便实现广度优先。更深入地考虑，可以设置双栈，第一个栈存储合取范式原有的单子句，第二个栈存储由单子句传播造成的单子句。双栈模式可以保证尽量使用1个单子句找到1个冲突集。

关于数据结构选择的实验内容帮助学生通过实践学习栈、数组、链式栈等相关内容，亦帮助学生培养和形成针对问题选择优化数据结构的思维和方法。

3实验评估

在正确求解的前提下，运行时间可衡量算法的性能好坏。时间越短，性能越好。运行时间的长短直接表现为搜索树的结点数和回溯数的大小，搜索树的分支数和回溯数越小，运行时间越短。表1列出了MaxSAT算法MaxsatzEF和Maxsatz两个算法在同样机器上运行算例集的时间对比。表2列出了计算相同算例，两个算法的搜索结点数、回溯数的对比。

4结语

基于最大可满足性问题的专业实验方案采用实际工业问题作为算例，利用命题逻辑建模、设计算法以及选择优化的数据结构。该方案涉及程序设计语言、离散数学、数据结构、计算机组成原理、算法分析与设计等多门计算机核心课程，有助于学生系统地掌握知识及其应用方法，更重要的是该方案向学生展示了一个完整的利用计算机解决实际问题的过程。

参考文献参考文献：

＼[1＼]陶影，张斌.数据结构实验教学应重视算法设计与分析能力的培养[J].实验室研究与探索，2008，27（12）：119122.

[2]STEPHEN A COOK.The complexity of theorem proving procedures[C].Proceedings of the 3rd annual ACM symposium on theory of computing，1971：151158.

[3]JOSEP ARGELICH， CHUMIN LI， FELIP MANYA，et al.Analyzing the instances of the MaxSAT evaluation[C].Proceedings of the 14th Theory and Application of Satisfiablity Testing，2011：360361.

[4]CHUMIN LI，MANYA FELIP，NOUREDINE MOHAMEDOU.Resolution based lower bounds in MAXSAT[J].Journal of Constraints， 2010， 15（4）：456484.

[5]刘燕丽，李初民，何琨.基于优化冲突集提高下界的MaxSAT完备算法[J].计算机学报，2013，10（36）： 20872096.

[6]OLIVIER DUBOIS，P ANDRE，Y BOYFKHAD.SAT versus UNSAT[J].DIMACS Series in Discrete Mathematics and Theoretical Computer Science，1996（2）：415436.

[7]余艳，刘燕丽.数据结构教学方法探讨[J].计算机教育，2013（9）：5658.

[8]田运生，刘维华，王景春.综合性设计性试验项目建设的探索与实践[J].实验技术与管理，2012，29（2）：126129.

[9]郝小江，繆志农，黄昆.基于DSP的数字信息处理实验设计[J].实验技术与管理，2012，29（2）：4447.

[10]易昆南， 于菲菲.在综合性、设计性实验中培养学生的创新能力[J].实验技术与管理，2007，24（8）：79.

责任编辑（责任编辑：孙娟）