Punch Powertrain is a company developing car components. They want to find automatically all solutions for sets of requirements on a sequence of components; attempts to do this by Prolog easily ran out of resources. Some first experiments to use a SAT/SMT solver instead look promising. The underlying problem consists of finding a graph of which every node is of some type, every type of nodes has a fixed degree, and there are restrictions on connections between different types. One challenge is symmetry reduction: describe the graphs in such a way that essentially the same solutions are not counted twice. A possible master project is to elaborate this further at the company (location Eindhoven), tuned towards their practical issues, and figure out to which order of magnitude this is feasible to be solved by SAT/SMT, or other approaches. Contact: Hans Zantema, h.zantema@tue.nl