A declarative approach to robust weighted Max-SAT

11 years 8 months ago
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...
Miquel Bofill, Dídac Busquets, Mateu Villar
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where PPDP
Authors Miquel Bofill, Dídac Busquets, Mateu Villaret
Comments (0)