Relaxations for compiled over-constrained problems

In many real-world settings, e.g. product configuration, constraint satisfaction problems are compiled into automata or binary decision diagrams, which can be seen as instances of Darwiche's negation normal form. In this paper we consider settings in which a foreground set of constraints can be added to a set of consistent background constraints, that are compactly represented in a compiled form. When the set of foreground constraints introduces inconsistencies with the background constraints we wish to find relaxations of the problem by identifying the subset of the foreground constraints that do not introduce inconsistency; such a subset is called a relaxation. This paper is organised in two parts. First, two novel algorithms for finding relaxations based on automata are presented. They find the relaxation that is consistent with the largest (or smallest) number of solutions from amongst the longest ones (first algorithm), or from amongst the set-wise maximal ones (second algorithm). Then, we generalise our results by identifying the properties that the target compilation language must have for our approach to apply. Finally, we show empirically that on average our algorithms can be more than 500 times faster than a current state-of-the-art algorithm.