Constraint Reasoning

Our mission is to lead the research on decision and optimisation procedures. Our approach involves fundamental work on new theories and constraints over different formalisms. Our algorithms are thought with parallelism in mind to adequately meet large scale computational resources. The results of our research impact many domains, in particular when the ability to search through a large set of possibilities and to find the ones that optimally match a set of given requirements is fundamental.

Research questions

	Parallel Satisfiability. How can we efficiently harness the power of multicore machines and massively parallel cloud-based HPC resources to disentangle the original NP-complete problem?
	Declarative Problem Solving. What is the link between how problems are logically described in a formal language, and how they are solved by algorithms?
	Satisfiability Modulo Theories. How can we extend Boolean satisfiability with combinations of background theories?

Application domains

	Configuration, Planning, and Scheduling. In manufacturing, customize orders, sequence and decide exact timing of operations to fulfil orders.
	Software and hardware verification. In software and hardware engineering, considers if a piece of software or hardware fully satisfies a set of given requirements.
	Emerging applications domains. Personal Assistants, Social Networks, Program Synthesis, Mobility, etc.