TY - GEN

T1 - Robust Weighted Partial Maximum Satisfiability Problem

T2 - 19th Pacific Rim International Conference on Artificial Intelligence, PRICAI 2022

AU - Sugahara, Tomoya

AU - Yamashita, Kaito

AU - Barrot, Nathanaël

AU - Koshimura, Miyuki

AU - Yokoo, Makoto

N1 - Funding Information:
Acknowledgements. This work is supported by JSPS KAKENHI Grant JP19H04175, JP20H00609, and JP22K19813.
Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

PY - 2022

Y1 - 2022

N2 - 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 Σ2P -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).

AB - 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 Σ2P -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).

UR - http://www.scopus.com/inward/record.url?scp=85144561614&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85144561614&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-20862-1_2

DO - 10.1007/978-3-031-20862-1_2

M3 - Conference contribution

AN - SCOPUS:85144561614

SN - 9783031208614

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 17

EP - 31

BT - PRICAI 2022

A2 - Khanna, Sankalp

A2 - Cao, Jian

A2 - Bai, Quan

A2 - Xu, Guandong

PB - Springer Science and Business Media Deutschland GmbH

Y2 - 10 November 2022 through 13 November 2022

ER -