Constraint programming is a paradigm for computing with mathematical relations named constraints. It is a declarative approach to describe many real-world problems including scheduling, vehicles routing, biology and musical composition. Constraint programming must be contrasted with procedural approaches that describe how a problem is solved, whereas constraint models describe what the problem is. The part of how a constraint problem is solved is left to a general constraint solver. Unfortunately, there is no solving algorithm efficient enough to every problem, because the search strategy must often be customized per problem to attain reasonable efficiency. This is a daunting task that requires expertise and good understanding on the solver's intrinsics. Moreover, higher-level constraint-based languages provide limited support to specify search strategies.
In this dissertation, we tackle this challenge by designing a programming language for specifying search strategies. The dissertation is constructed around two axes:
- A novel theory of constraint programming based on lattice theory.
- A programming language, called spacetime programming, building on lattice theory for its data structures and on synchronous programming for its computational model.
The first part formalizes the components of inference and search in a constraint solver. This allows us to scrutinize various constraint-based languages through the same underlying foundations. In this respect, we give the semantics of several paradigms including constraint logic programming and concurrent constraint programming using lattices. The second part is dedicated to building a practical language where search strategies can be easily composed. Compositionality consists in taking several distinct strategies and, via some operators, to compose these in order to obtain a new strategy. Existing proposals include extensions to logic programming, monadic constraint programming and search combinators, but all suffer from different drawbacks as explained in the dissertation. The original aspect of spacetime programming is to make use of a temporal dimension, offered by the synchronous paradigm, to compose and synchronize search strategies on a shared logical clock.
This paradigm opens the door to new and more complex search strategies in constraint programming but also in applications requiring backtracking search. We demonstrate its usefulness in an interactive computer-aided composition system where we design a search strategy to help the composer navigating in the state space generated by a musical constraint problem. We also explore a model checking algorithm where a model dynamically generates a constraint satisfaction problem (CSP) representing the reachability of some states. Although these applications are experimental, they hint at the suitability of spacetime programming in a larger context.