Revisiting Pseudo-Boolean solving for Constraint Programming

This work is situated in the ERC Consolidator Grant project 'Conversational Human-Aware Technology for Optimisation (CHAT-Opt)'. The goal of this PhD is to improve the underlying solving technology that is used in the ERC project. More specifically we will revisit pseudo boolean encodings and solvers for Constraint Programming models, building on our CPMpy library. The potential of pseudo boolean solving is that these solvers 1) are incremental and 2) use a stronger proof system than SAT solvers. The first point is a key requirement for our work on explainable constraint solving, where explanation techniques are most effective when using incremental solvers. The second point has the potential to significantly further speed up explanation algorithms, though the precise conditions and ways under which this solving technology outperforms standard SAT solvers is not yet fully understood. Furthermore, there is great potential in new explanation algorithms that more closely integrate and build on the capabilities of pseudo boolean solvers.