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