Tutorial: Quantified Boolean Formulas

Abstract:

Many application problems from artificial intelligence, verification, and formal synthesis can be efficiently encoded as quantified Boolean formulas (QBFs), the extension of propositional logic with quantifiers. This extension makes the QBF decision problem PSPACE-complete (in contrast to SAT which is NP-complete).Over the last years, much progress has been made concerning the theory and practice of QBF research. In this tutorial, we review the state of the art of QBF technology and show how to perform automated reasoning with QBFs.

Invited talk: Reasoning with SAT and Beyond

Abstract:

One of the biggest success stories of symbolic artificial intelligence is written by SAT solvers, i.e., by tools that answer the question if a given propositional formula is satisfiable or not. Despite the NP-hardness of SAT, modern solvers are able to decide huge formula instances from industrial application domains like formal verification. The performance boost of SAT solvers we have seen over the last 20 years only became possible by cleverly exploiting the problem structure of the formula, by a tight integration of powerful search and inference techniques, and advanced heuristics. Because of their power, SAT solvers are nowadays also the backend reasoning engines for solving decision problems beyond NP like QBF, SMT, and MaxSAT. 

In this talk, we shortly trace the story of SAT solving and show how SAT helps to solve problems beyond NP. We identify open challenges related to other branches of symbolic reasoning and artificial intelligence. 

Prescriptive Analytics: When data- and simulation-based models interact in a cooperative way

Abstract:

Prescriptive Analytics is an interdisciplinary topic in an interdisciplinary field, or put another way it is a synergistic hybridisation of various methods and algorithms from statistics, computer science, artificial intelligence, mathematics and operations research. Its aim is to provide optimized recommendations for action in various application areas. In this way, knowledge gained in the digital world is brought back to the real world, providing better and more efficient procedures, designs and processes.

Simulation and data-based models have several advantages and limitations. Simulation-based representations of reality can be very accurate; however, they are often too costly for the purpose of integration into powerful optimization methods. Data-based surrogate models on the other hand can be highly efficient in application – but may not be as accurate. Appropriate hybridizations of these approaches in terms of prescriptive analytics have the potential to support and complement each other and decisively advance research areas such as simulation-based optimization.

The presentation will include methodological research topics that are currently being pursued in the HEAL research group [https://heal.heuristiclab.com/] led by Affenzeller as well as concrete project results that have already found their way into economic and industrial applications.

Invited talk: SAT Solvers and Quantum Computing: Potential and Challenges

Abstract:

SAT or SMT solvers are well-established in conventional computing where they are used to solve a broad variety of problems, e.g., in the design of circuits and systems. With the emerging of quantum computers, it is natural to wonder whether the prospects of SAT-based solutions can also be materialized for this emerging technology. For one thing, many of the design tasks for quantum computing have been proven to be NP-hard—a class of problems for which SAT solvers are rather suited. Then again, quantum computing deals with quantum-mechanical concepts such as superposition and entanglement—easily rendering SAT unfeasible at a first glance. In this talk, we are investigating whether SAT solvers and quantum computing harbor potential; and, if so, what are the challenges in fully exploiting them.

Tutorial: Mathematical Model Checking in RISCAL

Abstract

Model checking is a technique that is well established in computer science for verifying the correctness of finite state systems (i.e., models of hardware or software systems with finite state spaces); the verification is performed with respect to specific safety properties such as the absence of runtime errors or with respect of general correctness properties that are typically specified in a variant of temporal logic. The principal advantage of model checking is that it is a fully automatic technique and demonstrates the violation of a property by a concrete countexample run.In this tutorial, we demonstrate how the RISCAL software can be utilized to enjoy similar benefits in a more general context, namely the design and analysis of mathematical theories over discrete domains and the specification and verification of algorithms that solve problems in these theories. RISCAL is a “mathematical model checker” based on a statically typed variant of first-order logic and set theory where all domains have parameterized but finite sizes. This allows to validate (respectively falsify) conjectures and problem solutions in specific small domains, before attempting to verify by proof their general correctness for domains of arbitrary size.We demonstrate these ideas by modeling and analyzing in live demonstrations example problems from various areas of discrete mathematics, algebra, and logic. The RISCAL software is freely available and the demonstration examples can be downloaded from the RISCAL web site (https://www.risc.jku.at/research/formal/software/RISCAL).

Tutorial: Application, Analysis, and Development of Metaheuristic Algorithms with HeuristicLab, an Open-source Optimization Environment for Research and Education 

Abstract:

HeuristicLab [1, 2] is an open-source environment for heuristic optimization that features several metaheuristic optimization algorithms as well as optimization problems. It is developed by the research group Heuristic and Evolutionary Algorithms Laboratory (HEAL) [3] of the University of Applied Sciences Upper Austria and is based on C# and Microsoft .NET. HeuristicLab is used as development platform for several research and industry projects (for example the Josef Ressel Centers SymReg [4] and adaptOp [5]) as well as for teaching metaheuristics in the study programs Software Engineering and Medical- and Bioinformatics in Hagenberg. Over the years HeuristicLab has become more and more known within the metaheuristic optimization community and is used by researchers and lecturers at different universities worldwide. This tutorial demonstrates how to apply, analyze, and develop metaheuristic optimization algorithms using HeuristicLab [1, 2]. It will be shown how to parameterize and execute evolutionary algorithms to solve combinatorial optimization problems (routing, scheduling) as well as data analysis problems (regression, classification). Participants will learn how to assemble different algorithms and parameter settings to a large-scale optimization experiment and how to execute such experiments on multi-core or cluster systems. Furthermore, the experiment results will be compared using HeuristicLab’s interactive charts for visual and statistical analysis to gain knowledge from the executed test runs. To complete the tutorial, it will be sketched briefly how HeuristicLab can be extended with further optimization problems and how custom optimization algorithms can be developed.

[1] https://dev.heuristiclab.com 

[2] https://github.com/heal-research/HeuristicLab 

[3] https://heal.heuristiclab.com 

[4] https://www.symreg.at

[5] https://www.adaptop.at

Tutorial: Conditional Rewriting in Theorema 2.0

Abstract

The Theorema system is a proof assistant based on Mathematica, one of the leading systems (not only) symbolic computation.The main aim of Theorema is “natural style”, both in input and in output. From Mathematicawe mainly use its highly programmable notebook interface and the pattern-based programming language. In contrast to other provers in and around the Wolfram/Mathematica-ecosystem, Theorema’s logical engine guiding the proofs does not use any of Mathematica’s builtin algorithms for manipulating symbolic expressions, but has its own language for predicate logic and a proof calculus similar to natural deduction in order to automatically generate human-like proofs. In this tutorial, we want to focus on conditional rewriting and explain its implementation and its applications in the frame of Theorema 2.0. The tutorial will mainly be based on a live demo of the system showing concrete examples of proofs as they are used in teaching logic with the help of Theorema.

Invited talk:  Implementation Techniques for Mathematical Model Checking

Abstract

The aim of the RISCAL software is the analysis of theories and algorithms over discrete domains as they arise in computer science, discrete mathematics, logic, and algebra. For this purpose, RISCAL provides an expressive specification language based on a strongly typed variant of first-order logic with a rich set of types and operations in which theories can be formulated and algorithms can be specified; nevertheless the validity of all formulas and the correctness of all algorithms is decidable. This is because all RISCAL types have finite sizes and thus the underlying model is finite; the sizes of the types and thus of the model is configurable by model parameters. RISCAL thus represents a tool for the automated validation and (more important) falsification of conjectures, in order to avoid fruitless attempts to prove invalid statements. The system has been mainly developed for educational purposes but it also has been applied in research.

In this talk, we present and compare the various decision techniques that have been applied in the implementation of RISCAL. The original implementation was based on “semantic evaluation” where all syntactic phrases of the specification language were translated into an executable representation of their (generally nondeterministic) denotational semantics; while this mechanism is reasonably efficient, its main advantage is actually its transparency: it gives easily rise to visual representations of the semantics and to the generation of counterexamples for invalid conjectures. Later (by Franz-Xaver Reichl), an alternative decision mechanism was developed in the form of a translation of RISCAL into the SMT-LIB theory QF_UFBV (unquantified formulas over bit vectors with uninterpreted sort and function symbols) which can be decided by various SMT solvers. While this decision mechanism is generally much more efficient and allows the analysis of much larger domains, there are also situations when it is inferior to the semantics-based approach; we discuss the pros and cons of both approaches based on both synthetic and real-world benchmarks.

These techniques are complemented by the recent addition of an implementation (by Ágoston Sütő) of the verification of transition systems with respect to linear temporal logic specifications by their translation to finite automata.

Tutorial: Natural Language Processing for Industrial Applications

Tutorial summary

After completing this tutorial session you will…

• …know how computers process human language
• …know the most common NLP-tasks and how to create value for your use-case
• …be aware about challenges and possible solutions
• …have an overview of the NLP-toolbox (models, python libraries and other resources) and how to get started

Invited talk: Complex Network Analysis using AI algorithms

Abstract

The network science field has witnessed a tremendous growth in recent years due to the increasing availability of massive datasets modelled using complex networks, the advances made in the field of Artificial Intelligence (AI) and the demonstrated successes of network-based theories in domains such as biology, engineering, health and social sciences. Networks provide powerful models for the analysis and understanding of complex phenomena, offering a new perspective on data by creating structures and links that can be visualized and analysed using specialized algorithms. Nevertheless, networks pose significant challenges related to system functionality through node interactions, understanding network processes and predicting behaviour.

This talk provides an introduction to the network science field, covering important tasks in complex network analysis, including the identification of important nodes in the network, outlining the cycles and relevant paths in the network, detection of communities and network dynamics. For each of these problems, relevant methods and AI algorithms will be presented and discussed based on real examples and results for different types of networks.