Return of the JTMS: Preferences Orchestrate Conflict Learning and Solution Synthesis

We use a lexicographical preference order on the problem space to combine solution synthesis with conflict learning. Given two preferred solutions of two subproblems, we can either combine them to a solution of the whole problem or learn a 'fat' conflict which cuts off a whole subtree. The approach makes conflict learning more pervasive for Constraint Programming as it well exploits efficient support finding and compact representations of Craig interpolants.