[4F1-OS-8a] AIと制約プログラミング(1/2)

[4F1-OS-8a-04] R-MaxSAT : MaxSAT with adversary

Kaito Yamashita¹, 〇Tomoya Sugahara¹, Miyuki Koshimura¹, Makoto Yokoo¹ (1. Kyushu University)

Keywords:MaxSAT, Clique Partition Problem, robust solution

This paper presents a new problem called Robust weighted Partial Maximum Satisfiability (R-PMaxSAT), which is an extension of Robust MaxSAT (R-MaxSAT) whose decision version is Sigma2P-complete.
In R-MaxSAT (or R-PMaxSAT), a problem solver called the defender expects to maximize the number of satisfied clauses (or the sum of their weights) as a standard MaxSAT, although the obtained solution must be robust.
We presume an adversary called the attacker will modify some variables after the defender decides a solution.
R-PMaxSAT can formalize a robust Clique Partitioning Problem (robust CPP), where CPP has many real-life applications.
Then, we introduce two algorithms to solve R-PMaxSAT, by utilizing a modern SAT solver or a QBF solver as a subroutine.
Our experimental results show that we can obtain optimal solutions within reasonable time for randomly generated R-MaxSAT instances and robust CPP instances based on CPP benchmark problems.