Description

BetterBe is a company, based in Enschede, that provides webservices to automotive lease companies, in particular, calculates the price of a particular lease car.

Calculating this price is more complex than one may think, merely because of the large number of intricate dependencies between the various options. For instance: if you opt for a sports package, you cannot choose certain radios (reason: the leather steering wheel coat does not have the right holes for the radio buttons). There are hundreds of such dependency rules. Therefore, figuring out if a certain set of option is feasible, and determine its price, is non-trivial.

SAT solving seems a natural technology to tackle this challenge: SAT is an advanced method to determine whether or not a logical formula is satifiable or not. Advanced tool support, such as MathSat and Z3, is available. Existing SAT solvers, however, are good as solving large queries. What is needed here, is to solve a large number of small queries.

Thus, the goal of this project is to (1) model the price calculations as a SAT solving problem, and (2) see if SAT solving techniques can be taylored to the specific case of running many small queries.