A SAT-Based Tool for Solving Configuration Problems

Configuration problems typically describe situations in which a user has to buy a configurable product selecting its features. The user wants to configure the product in the best way, selecting most of his favourite features and options for the product, but taking into account also the cost and other aspects. The idea is to find the best configuration of the product. Configuration problems are optimization problems in which the “best” solution is found according to some criterion, which in our case is based on the user preferences. They have application in scheduling, configuration, planning, timetabling tasks. For a simple example of configuration problem we can consider a laptop with some of its features, including the screen size, the screen model, the processor model, the video card and the webcam. The choice of the product features and the budget of the user are expressed by rules, called constraints. A configuration problem describes a product defining variables (the features of the product) and constraints, which are expressions involving the variables. Constraints are necessary to deny some configurations (think for example a very expensive laptop). The constraints are split into two sets, the set of the constraints that must be satisfied (background) and the set of the other remaining constraints (foreground), which can be satisfied or relaxed. In the laptop example the background includes the fundamental features and the constraint regarding the budget, while the foreground includes the optional features. The work explained here is a tool for solving configuration problems (X, D, B, F) where X is a set of variables, D is the set of the variables domains, B is the background and F is the foreground. In particular the tool implements the QuickXplain algorithm (§3.3) for configuration problems on which is defined a binary preference relation < among the foreground constraints. This relation expresses the fact that some constraints are more important than other ones, and the satisfaction of the first ones is preferred to the satisfaction of the latter ones. The QuickXplain algorithm returns the preferred conflict and the preferred relaxation. Given a configuration problem (X, D, B, F, <), the preferred relaxation is a subset of F which is consistent with respect to B, and maximizes the selection of the most important constraints according to <, while the preferred conflict is a subset of F which is not consistent with respect to B, and minimizes the selection of the least important constraints according to <. The problems of finding the preferred relaxation and the preferred conflict for a configuration problem are optimization problems that, in order to compute the best"