论文部分内容阅读
最大可满足性问题(MaxSAT)是人工智能领域研究的核心问题之一,很多复杂的实际问题都可以通过MaxSAT建模并求解,对于MaxSAT问题的研究具有理论和实际的双重意义。近些年,随着科学研究的进步和工业技术的发展,MaxSAT问题的规模成倍增长。为满足新的MaxSAT问题求解的需求,本文基于布尔博弈模型提出两个适用于不同规模MaxSAT实例求解的博弈算法,包括用于求解一般规模MaxSAT实例的基本博弈算法bgmaxsat和用于求解大规模MaxSAT实例的分组博弈算法bgmaxsat_m。本文的主要工作总结为以下四点。(1)我们提出一种将MaxSAT实例映射为布尔博弈模型的建模方法,通过博弈参与者的策略选择过程来模拟MaxSAT实例中的变量赋值过程。博弈参与者的策略基于重新定义的目标函数和收益计算函数进行选择,并依据其他参与者的策略不断更新。(2)针对MaxSAT问题的特征,我们对经典布尔博弈模型进行改进,提出基于动态收益矩阵的动态博弈模型。在动态博弈模型中,参与者的收益矩阵在博弈过程中实时变化,使得所有参与者都能够按照自身的目标函数快速收敛。基于动态博弈模型,我们提出求解一般规模MaxSAT实例的基本博弈算法bgmaxsat。(3)针对大规模MaxSAT实例产生大量博弈参与者的问题,我们提出一种新的博弈参与者联盟构建方法。我们基于无向图重建博弈参与者间的关系,将相互间无关系的参与者划分为一组来构建联盟,从而有效降低博弈规模。(4)基于博弈参与者联盟,我们提出求解大规模MaxSAT实例的分组博弈算法bgmaxsat_m。在bgmaxsat_m算法中,我们将博弈的基本单位设定为参与者联盟,并将信息共享通道仅设定在联盟之间。在实验部分,我们基于4个测试数据集进行了多组对比实验。首先,我们在846个一般规模MaxSAT实例上评估bgmaxsat算法,并与CCLS2016、Swcca-ms、ahmaxsat1.55三个最新算法进行对比。实验结果表明,在求解一般规模的MaxSAT实例时,bgmaxsat算法的性能与CCLS2016算法相近,其分别在不同分类的实例上各占优势,同时优于Swcca-ms算法和ahmaxsat1.55算法。其次,我们在100个变量规模超过105的大规模MaxSAT实例上评估bgmaxsat_m算法,并与CCLS2016、wbo、Open-wbo、pwbo、CnC-LS五个最新算法进行对比。实验结果表明,在求解大规模MaxSAT实例时,bmgaxsat_m算法的性能在所有分类的实例上均明显优于CCLS2016算法、wbo算法和pwbo算法,并且在随机分类的实例上优于Open-wbo算法和CnC-LS算法,而仅在部分工业分类的实例上不及Open-wbo算法和CnC-LS算法。