Interactive Configuration with Regular String Constraints

摘要

In this paper we present a generalization of the problem of interactive configuration. The usual interactive configuration problem is the problem of, given some variables on small finite domains and an increasing set of assignment of values to a subset of the variables, to compute for each of the unas-signed variables which values in its domain that participate in some solution for some assignment of values to the other unassigned variables. In this paper we consider how to extend this scheme to handle infinite regular domains using string variables and constraints that involves regular-expression checks on the string variables. We first show how to do this by using one single DFA. Since this approach is vastly space consuming, we construct a data structure that simulates the large DFA and is much more space efficient. As an example a configuration problem on n string variables with only one solution in which each string variable is assigned a value of length k the former structure will use Ω(k~n) space whereas the latter only need O(kn). We also show how this framework can be combined with the recent BDD techniques to allow both boolean, integer and string variables in the configuration problem.