What is the link between how problems are logically described in a formal language, and how they are solved by algorithms?

# Goals of the Project

Hard decision and optimization problems are ubiquitous. They arise from questions as diverse as:

- How do we route our fleet of vehicles?
- Is there an input that will cause a buffer overflow in this program?
- What changes to the design of this building would most effectively reduce its energy consumption?
- To which social network users do we give free trial versions of our new App in order to get mazimal buzz?

For such questions computational tools are indispensible.

Decision and optimization problems can often be formulated using mathematical formulas, or other machine-processable languages. This approach allows us to develop *general reasoning tools* that do not solve a specific problem but, rather, are able to solve any problem described in the formal language. With this "declarative approach to Problem Solving", developing solutions to hard problems becomes significantly easier: the user is only asked to describe her problem, while with usual programming languages she'd be asked to describe how to solve it.

The goal of this project is to develop tools for Declarative Problem Solving, and to better understand the interplay between the language aspect (*how do people express a problem in a formal language?*) and the algorithmic aspect (*how do we solve the described problem?*). We focus on the following questions:

- How do we make it easy for non-specialists to model problems?
- What are good models, i.e.: What makes a model hard / easy to solve? How do we automatically transform bad models into good ones?
- How do we design decision tools for problems that are hard-to-model: problems where the data are not known with certainty, problems where the system is described by a simulator or piece of software rather than equations.

- Lucas Bordeaux, Mikolas Janota, Joao Marques-Silva, and Pierre Marquis, On Unit-Refutation Complete Formulae with Existentially Quantified Variables, in
*Principles of Knowledge Representation and Reasoning (KR 2012)*, Association for the Advancement of Artificial Intelligence, June 2012 - Lucas Bordeaux and Joao Marques Silva, Knowledge Compilation with Empowerment, in
*38th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM)*, Springer Verlag, 2012