Analyzing Infeasible Constraint Systems.

Constraint systems, problems defined by sets of variables and constraints affecting the allowed assignments to those variables, arise in a wide range of real-world problems, from planning and scheduling to digital logic circuit verification. These problems have been studied widely in computer science and operations research, and a great deal of research has gone into developing algorithms that solve them quickly, producing assignments to variables that satisfy all of a system's constraints. Many constraint systems turn out to have no satisfying assignments -- they are said to be overconstrained or infeasible -- and work on analyzing these instances is much less mature. It is in this area that this work lies. Most work on analyzing infeasibility has focused on producing singular, approximate, partial views of the infeasibility of a given problem; a distinguishing feature of this work is that it is focused on complete analyses. We have developed algorithms that compute the full structure of a problem's infeasibility in the form of minimal correction sets (MCSes) and minimal unsatisfiable subsets (MUSes), both of which are subsets of a system's constraints that irreducibly describe part of its infeasibility. The value of these complete analyses has been demonstrated by applications of this work to two different logic circuit verification tasks, in which the complete views these algorithms produce have been shown to be critical for performance. Spurred partially by the needs of the industrial applications and also by theoretical considerations regarding the innate intractability of the given problems, extensions of these algorithms have been developed in several directions, enhancing performance by integrating partial, approximate analyses as guides, solving related problems that avoid the intractability while still providing more information than the singular views offered by other work, and generally exploring the space of infeasibility analysis in novel ways. Overall, this work helps to expand the field of constraint system research with new tools for analyzing infeasibility. This research, which has been kept as broadly-applicable as possible, serves as a base, opening up complete infeasibility analysis to researchers across the field of constraint research.PhDComputer Science & EngineeringUniversity of Michigan, Horace H. Rackham School of Graduate Studieshttp://deepblue.lib.umich.edu/bitstream/2027.42/63772/1/liffiton_1.pd