University of Twente Student Theses


Determining the Satisfiability of Car Configuration Models in a Repetitive Manner

Brunsveld, R.D. (2019) Determining the Satisfiability of Car Configuration Models in a Repetitive Manner.

[img] PDF
Abstract:Vehicles can have many different options and configurations. Not all combinations of these options are compatible. 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 calculate the lowest price. To use MaxSAT solving we have to encode the car configuration models of BetterBe into MaxSAT problems. 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. The proposed modifications do not provide any reduction of the execution time.
Item Type:Essay (Master)
BetterBe, Enschede, Netherlands
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page