R-MaxSAT : MaxSAT with adversary

DOI

Bibliographic Information

Other Title
  • R-MaxSAT : 敵対者が存在する MaxSAT

Description

<p>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.</p>

Journal

Keywords

Details 詳細情報について

Report a problem

Back to top