Description

Vehicles can have many different options and configurations. Not all combinations of these options are compatible. For example, a car can not have blue and red bodywork at the same time. To check whether a vehicle has a set of options which is compatible, BetterBe has implemented a solver which checks these options and allows customers of lease companies to configure their vehicles. A downside of this solver is the performance and maintainability.  Hence, we study here whether we can use constraint solving techniques to replace the solver of BetterBe.

A suitable technique is the use of a MaxSAT solver. A MaxSAT solver is able to determine the satisfiability of the car configuration and the lowest price. To use MaxSAT solving we have to encode the car configuration models of BetterBe into MaxSAT problems. This is done in collaboration with experts of BetterBe. In this thesis, we propose to use an incremental MaxSAT algorithm which can handle assumptions. This algorithm can solve the same MaxSAT problem with different assumptions without initialising a MaxSAT solver for every set of assumptions. Furthermore, we implement and compare several modifications.

We find that the proposed algorithm solves the car configuration problems with a similar performance as the dedicated solver of BetterBe. Because the algorithm is less flexible and BetterBe has provided underspecified car configurations, some results differ from BetterBe, but are not considered incorrect. The proposed modifications do not provide any reduction of the execution time. This is mostlikely due to the increased clause database, which leads to a higher execution time of the SAT solver.