Name: Bart Helvert
Afiliation: Eindhoven University of Technology & Siemens Industry Software (SISW)
Abstract
Many applications from formal methods and artificial intelligence use machine reasoning solvers to solve computationally-hard problems. There are various types of solvers with varying performance for different types of problems, and it is not always clear which solver technology is most appropriate. Comparing different solvers is difficult, because every solver provides its own unique API. Existing solutions to this problem exist, but often only support a sub-class of solvers or are implemented as an external DSL. This report is a master thesis preparation that sketches the techniques and technology used in the machine reasoning domain and proposes a solver agnostic API in the form of a C++ interface.