A Solver Agnostic Incremental Machine Reasoning Interface

  • Bart van Helvert

Student thesis: Master


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.
Date of Award19 Jul 2021
Original languageEnglish
SupervisorMark G.J. van den Brand (Supervisor 1), Cesar Santos (External coach) & Mauricio Verano Merino (Supervisor 2)

Cite this