Efficient Incrementality in Learning Solvers

Reasoning, constraint solving and optimisation technologies have made remarkable progress over the last two decades. A number of formalisms like Boolean satisfiability (SAT), satisfiability modulo theories (SMT) and their optimisation extensions (MaxSAT and MaxSMT) as well as constraint programming and optimisation (CP) and mixed-integer linear programming (MILP) can be seen as success stories in computer science. Although the efficiency of the state-of-the-art decision and optimisation procedures hinges on a wealth of sophisticated heuristic mechanisms, the key part driving their exceptional practical performance, is normally attributed to their learning capabilities. A learning solver gradually deduces and remembers new information about the decisions previously made, which can be reused in the future to prune the search space and to push the overall performance of the solver. Learning new information during search can be of help not only for solving one problem instance but also in common practical scenarios when a solver needs to be used "incrementally" when dealing with a sequence of "similar" problem instances.

This project is devoted to tackling the challenges arising in the incremental use of a learning solver applied to various practical problems. In particular, the project will develop novel techniques for the incremental use of core-guided MaxSAT and CP solvers in the context of a series of optimisation queries. A few sources of the target optimisation problems will be considered. To mention a few, the project will focus on (1) combining abstraction refinement and optimisation, (2) dealing with multi-objective optimisation, (3) optimisation and user interaction, (4) optimisation in the context of knowledge compilation (e.g. computing smallest representations of AI and ML systems), (5) problems arising from problem decomposition, where subproblems are typically resolved multiple times with small changes.