Using Symmetries to Lift Satisfiability Checking

We analyze how symmetries can be used to compress structures (also known as interpretations) onto a smaller domain without loss of information. This analysis suggests the possibility to solve satisfiability problems in the compressed domain for better performance. Thus, we propose a 2-step novel method: (i) the sentence to be satisfied is automatically translated into an equisatisfiable sentence over a ``lifted'' vocabulary that allows domain compression; (ii) satisfiability of the lifted sentence is checked by growing the (initially unknown) compressed domain until a satisfying structure is found. The key issue is to ensure that this satisfying structure can always be expanded into an uncompressed structure that satisfies the original sentence to be satisfied. We present an adequate translation for sentences in typed first-order logic extended with aggregates. Our experimental evaluation shows large speedups for generative configuration problems. The method also has applications in the verification of software operating on complex data structures. Further refinements of the translation are left for future work.

Applying Incremental Answer Set Solving to Product Configuration

In this paper, we apply incremental answer set solving to product configuration. Incremental answer set solving is a step-wise incremental approach to Answer Set Programming (ASP). We demonstrate how to use this technique to solve product configurations problems incrementally. Every step of the incremental solving process corresponds to a predefined configuration action. Using complex domain-specific configuration actions makes it possible to tightly control the level of non-determinism and performance of the solving process. We show applications of this technique for reasoning about product configuration, like simulating the behavior of a deterministic configuration algorithm and describing user actions.

Rail Topology Ontology: A Rail Infrastructure Base Ontology

Engineering projects for railway infrastructure typically involve many subsystems which need consistent views of the planned and built infrastructure and its underlying topology. Consistency is typically ensured by exchanging and verifying data between tools using XML-based data formats and UML-based object-oriented models. A tighter alignment of these data representations via a common topology model could decrease the development effort of railway infrastructure engineering tools. A common semantic model is also a prerequisite for the successful adoption of railway knowledge graphs. Based on the RailTopoModel standard, we developed the Rail Topology Ontology as a model to represent core features of railway infrastructures in a standard-compliant manner. This paper describes the ontology and its development method, and discusses its suitability for integrating data of railway engineering systems and other sources in a knowledge graph. With the Rail Topology Ontology, software engineers and knowledge scientists have a standard-based ontology for representing railway topologies to integrate disconnected data sources. We use the Rail Topology Ontology for our rail knowledge graph and plan to extend it by rail infrastructure ontologies derived from existing data exchange standards, since many such standards use the same base model as the presented ontology, viz., RailTopoModel.

Consistency-based Merging of Variability Models

Globally operating enterprises selling large and complex products and services often have to deal with situations where variability models are locally developed to take into account the requirements of local markets. For example, cars sold on the U.S. market are represented by variability models in some or many aspects different from European ones. In order to support global variability management processes, variability models and the underlying knowledge bases often need to be integrated. This is a challenging task since an integrated knowledge base should not produce results which are different from those produced by the individual knowledge bases. In this paper, we introduce an approach to variability model integration that is based on the concepts of contextual modeling and conflict detection. We present the underlying concepts and the results of a corresponding performance analysis.

OOASP: Connecting Object-oriented and Logic Programming

Most of contemporary software systems are implemented using an object-oriented approach. Modeling phases -- during which software engineers analyze requirements to the future system using some modeling language -- are an important part of the development process, since modeling errors are often hard to recognize and correct. In this paper we present a framework which allows the integration of Answer Set Programming into the object-oriented software development process. OOASP supports reasoning about object-oriented software models and their instantiations. Preliminary results of the OOASP application in CSL Studio, which is a Siemens internal modeling environment for product configurators, show that it can be used as a lightweight approach to verify, create and transform instantiations of object models at runtime and to support the software development process during design and testing.

(Re)configuration based on model generation

Reconfiguration is an important activity for companies selling configurable products or services which have a long life time. However, identification of a set of required changes in a legacy configuration is a hard problem, since even small changes in the requirements might imply significant modifications. In this paper we show a solution based on answer set programming, which is a logic-based knowledge representation formalism well suited for a compact description of (re)configuration problems. Its applicability is demonstrated on simple abstractions of several real-world scenarios. The evaluation of our solution on a set of benchmark instances derived from commercial (re)configuration problems shows its practical applicability.