Solving Over-Constrained Problems with SAT

Abstract. We present a new generic problem solving approach for overconstrained problems based on Max-SAT. We first define a clausal form formalism that deals with blocks of clauses and distinguish between hard and soft blocks. We then present two Max-SAT-based solvers for our formalism and an experimental investigation.

• Type: Conference
• Year: 2005
• Where: CP
• Authors: Josep Argelich, Felip Manyà
• Keywords: Clausal Form Formalism, CP 2005, Problem Solving Approach, Programming Languages, Soft Blocks