Reasoning about Conditional Constraint Specifications

Product configuration is a major industrial application domain for constraint satisfaction techniques. Conditional constraint satisfaction problems (CCSPs) have been developed to represent configuration problems in a natural way. CCSPs are like constraint satisfaction problems (CSPs), but they may also include potential variables, which might or might not exist in any given solution, as well as classical variables, which are required to take a value in every solution. CCSPs model, for example, options on a car, for which the style of sunroof (a variable) only makes sense if the car has a sunroof at all. We show that existing techniques from formal methods and answer set programming can be used to naturally model CCSPs. We demonstrate configurators in both approaches. An advantage of these approaches is that the model builder does not have to reformulate the CCSP into a classic CSP, converting potential variables into classical variables by adding a ¿does not exist¿´ value and modifying the problem constraints. Our configurators automatically reason about the model itself, enumerating all solutions and discovering several kinds of model flaws.