In this paper, we consider the energy-efficient coordination of a set of appliances in a smart-building. We introduce a theoretical formulation of the coordination problem and an Integer Linear Programming model for its resolution. Our formalization is complemented by an analysis of the properties and limits of the model. We also define a practical smart-building setting in which our formalization holds. Finally, we conduct several experiments with realistic data and we make a scalability and sensitivity analysis. The experimental results correspond to emulation on an industrial infrastructure for smart-buildings, the one of Qarnot computing. They are obtained in using the API of the company. They show that we can quickly solve the problem for small and medium-sized buildings and for realistic settings. They also open interesting questions regarding the optimal model of control in future intelligent buildings. Should residents let a collective intelligence to decide on the optimal control of its appliance or is it more appropriate that the user decides by itself?