We propose a technique for solving a type of overconstrained resource allocation problem that is commonly encountered at the heart of many realworld planning and scheduling applications. This type of resource allocation problems are characterized by what we call modular constraints: good solutions are those that guarantee the allocation of resources to tasks that can satisfy all of its requirements and avoid generating assignments that result in broken or partially satisfied tasks. Using SAT and Pseudo-Boolean encodings, we show that a typical or plain encoding results in solutions with a large number of broken tasks while our proposed encodings, by taking into account the modular constraint structure of the problems, guarantee good solutions. In addition, we show that the phase-transition characteristics of the resulting SAT formulas can be used to rapidly estimate the maximum number of satisfiable tasks. This information can be very valuable in the design and implementation of transition-aware solvers.
分享
引用
