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.
|
PDF
1MB |
| 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) |
| Clients: | BetterBe, Enschede, Netherlands |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science MSc (60300) |
| Link to this item: | https://purl.utwente.nl/essays/78001 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page