A declarative approach to robust weighted Max-SAT

The presence of uncertainty in the real world makes robustness to be a desired property of solutions to constraint satisfaction problems. Roughly speaking, a solution is robust if it can be easily repaired when unexpected events happen. This issue has already been addressed in the frameworks of Boolean satisfiability (SAT) and Constraint Programming (CP). Most works on robustness implement search algorithms to look for such solutions instead of taking the declarative approach of reformulation, since reformulation tends to generate prohibitively large formulas, especially in the CP setting. On the other hand, recent works suggest the use of SAT and Max-SAT encodings for solving CP instances. In this paper we present how robust solutions to weighted Max-SAT problems can be effectively obtained via reformulation into pseudo-Boolean formulae, thus providing a much flexible approach to robustness. We illustrate the use of our approach in the robust combinatorial auctions setting and prov...

• Type: Journal
• Year: 2010
• Where: PPDP
• Authors: Miquel Bofill, Dídac Busquets, Mateu Villaret
• Keywords: Max-SAT, PPDP 2010, Programming Languages, Robustness, Solutions