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", here called preferred, consider a lexicographic extension of the preference relation <. Relaxations and conflicts are dual concepts defined in §3.2.1. The implemented tool returns also a solution for the configuration problems, namely an assignment variables-values that satisfies the constraints contained in the background and in the preferred relaxation. QuickXplain is a recursive and dichotomic algorithm that uses a CSP consistency checker to see whether a set of constraints has solutions or not. The idea and the approach here is to use a SAT solver as CSP solver, solving the satisfiability of the formulas encoded from the constraints defined in the configuration problems. MiniSat, an efficient SAT solver, is used for this purpose. The problems taken into account are written in CP language (§3.4.1), and compose the Configuration Benchmarks Library (CLib) [7]. The tool is implemented in Java and encodes the constrains of every configuration problem into a propositional formula (an instance of the SAT problem) which can solved by a SAT solver. I started this work in the College of Computer Science and Technology at the Jilin University [2], in Changchun (China). In 2008 I studied there as exchange student under the framework of the EASTWEB project [1]. The chapters of the first part give a brief introduction on the topics related to this work, mainly SAT and CSP. The second part focuses on the tool, explaining its functionalities and components