Daniel Sabin and Eugene C. Freuder
In this paper we present resource optimization methods for solving efficiently synthesis problems in a constraint-based framework. We obtain a tight lower bound of the problem optimum by adding redundant constraints that take into account the "wastage" in a partial solution. Abstraction through focusing on relevant features permits added interchangeability to deal with equivalent sets of partial solutions. Combining these two ideas allows us to discover fast the optimal solution, and also to prove very quickly its optimality.