Learning Modulo Theories

Many real-world applications require reasoning over hybrid domains involving combinations of continuous and discrete variables and their relationships. Being able to precisely specify all constraints and their respective importance beforehand is often infeasible for the most experienced designer, let alone for a typical decision maker. In this chapter we discuss Learning Modulo Theories (LMT), a learning framework capable of dealing with hybrid domains by combining structured learning with Satisfiability Modulo Theory (SMT) techniques. LMT incorporates SMT solvers and their extensions for optimization as inference engines within learning algorithms. The learning stage automatically identifies the relevant constraints and their respective weights among a set of candidates. The framework can be cast in the structuredoutput learning paradigm, where the task is learning the structure of the problem from a set of noisy instances, or as a preference elicitation task, where a decision maker is involved in an interactive optimization loop aimed at generating the most preferred solution. We report experimental results highlighting the potential of the method in automated design and recommendation scenarios.