**Financial support through the following projects:**

UIDB/00297/2020

UID/MAT/00297/2019

UID/MAT/00297/2013

PEst-OE/MAT/UI0297/2014

PEst-OE/MAT/UI0297/2011

Wednesday, 18 February 2015, 1:00 p.m.

Lecturer: Prof. Dr. Wolfgang Küchlin (Symbolic Computation Group Informatik, Universität Tübingen, Germany, Steinbeis Technology Transfer Center STZ OIT)

Title: "Logical Reasoning in the Auto Industry"

Local: Room 1.13, Edifício VII

Faculdade de Ciências e Tecnologia, Quinta da Torre, Caparica

Abstract: Propositional Logic is widely used by Automobile Manufacturers (e.g. Volkswagen, Daimler, AUDI, BMW, General Motors, Opel, Renault) to solve configuration problems. The problems are solved on two levels: High-Level Configuration (HLC) regulates how a customer can configure her car, i.e. which equipment options can be ordered simultaneously. Low-Level Configuration (LLC) regulates which individual parts are needed in order to build a specific customer order, i.e. a specific variant of a car.

HLC is given by a set of Boolean constraints over all equipment options. Each true/false assignment to the options which satisfies all HLC constraints gives an admissible car order. For premium German cars, the number of possible customer orders is typically in the range of 10^{20} – 10^{50}. LLC is given by a Bill of Materials (BOM) which lists all parts for all possible variants. The condition under which a specific part is needed for a specific car variant is given by a Boolean formula which is attached to the part.

Even small „trivial“ mistakes in the formulas can lead to serious problems at the assembly line. We show how common defects in both HLC and LLC can be detected by automated Boolean reasoning, in particular satisfiability solving (SAT-Solving). E.g., how can we prove that each car variant will select exactly one of 300 possible steering wheels in the BOM? How can we prove which equipment options are available in which countries?

This application poses two main challenges: First, the mapping of each application problem to a verification problem in Boolean Algebra. Second, the efficient solution of millions of instances of verification problems in real time. Our algorithms are implemented by STZ OIT in in commercial software packes which are in regular use by three German premium car manufacturers.