[2E3-OS-13b] AIと制約プログラミング(2/3)

[2E3-OS-13b-05] ADSAT: MaxSAT with adversary

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

Keywords:SAT, MaxSAT

This paper deals with ADSAT (Attacker Defender SAT), in which there are two persons: attacker and defender. The defender's objective is to maximize the number of satisfied clauses while the attacker's objective is to maximize the number of falsified clauses. The goal of this study is to find an optimal solution for the defender against all possible attacks.
We treat the problem as robust MaxSAT in which we aim to find an assignment that maximize the satisfaction even if someone flips the values of some variables in the assignment. A decision version of this problem was shown to be Σ^P₂-complete.
In the previous research, the IBR (Iterated Best Response) algorithm has been proposed for solving ADSAT. However, it is difficult to find the optimal solution in a practical time even for small problems.
In this paper, we propose the AE (Attack Enumeration) algorithm to obtain a non-exact solution for ADSAT. AE can efficiently obtain an approximate solution if the possible attack is limited. We experimentally compare the performance of both algorithms with several instances.