Robust Weighted Partial Maximum Satisfiability Problem: Challenge to Σ2P-Complete Problem
Robust Weighted Partial Maximum Satisfiability Problem: Challenge to Σ2P-Complete Problem
复制标题
鲁棒加权部分最大可满足性问题：对Σ2P完全问题的挑战
DOI：
10.1007/978-3-031-20862-1_2
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Yokoo Makoto
中科院分区：
文献类型：
--
作者：
Sugahara Tomoya;Yamashita Kaito;Barrot Nathanael;Koshimura Miyuki;Yokoo Makoto
本文介绍了一个新的问题--稳健极大可满足性问题(R-MaxSAT)及其推广--稳健加权部分极大可满足性问题(R-PMaxSAT)。在R-MaxSAT(或R-PMaxSAT)中，一个名为Defender的问题求解器希望最大化满足子句的数量(或它们的权重之和)，作为标准的MaxSAT/部分MaxSAT问题，尽管她必须确保所获得的解是健壮的(在本文中，我们使用代词“她”来表示防御者，“他”来表示攻击者)。我们假设一个名为攻击者的对手在防御者选择解决方案后会反转一些变量。R-PMaxSAT可以形式化描述健壮的团划分问题(Robust CPP)，而健壮的团划分问题在现实生活中有很多应用。我们首先证明了R-MaxSAT的决策版本是-完备的。然后，我们开发了两个算法来求解R-PMaxSAT，使用最先进的SAT求解器或量化布尔公式(QBF)求解器作为子程序。实验结果表明，对于随机生成的具有30个变量和150个子句的R-MaxSAT实例(在S 40以内)和基于60个顶点的CPP基准问题的R-PMaxSAT实例(在S 500以内)，我们可以在合理的时间内获得最优解。
This paper introduces a new problem called the Robust Maximum Satisfiability problem (R-MaxSAT), as well as its extension called the Robust weighted Partial MaxSAT (R-PMaxSAT). In R-MaxSAT (or R-PMaxSAT), a problem solver called defender hopes to maximize the number of satisfied clauses (or the sum of their weights) as the standard MaxSAT/partial MaxSAT problem, although she must ensure that the obtained solution is robust (In this paper, we use the pronoun “she” for the defender and “he” for the attacker). We assume an adversary called the attacker will flip some variables after the defender selects a solution. R-PMaxSAT can formalize the robust Clique Partitioning Problem (robust CPP), where CPP has many real-life applications. We first demonstrate that the decision version of R-MaxSAT is-complete. Then, we develop two algorithms to solve R-PMaxSAT, by utilizing a state-of-the-art SAT solver or a Quantified Boolean Formula (QBF) solver as a subroutine. Our experimental results show that we can obtain optimal solutions within a reasonable amount of time for randomly generated R-MaxSAT instances with 30 variables and 150 clauses (within 40 s) and R-PMaxSAT instances based on CPP benchmark problems with 60 vertices (within 500 s).