I will talk about the problem of allocating a divisible budget among different projects, based on agents' preferences given as approval ballots over the projects. That is, we will study voting rules that take approvals as input and return a probability distribution over alternatives. We will discuss some promising voting rules for this setting (e.g. Nash, or maximizing utilitarian welfare subject to fairness) and the properties that they satisfy (e.g. efficiency, strategyproofness, fairness). Our main result settles a long-standing open question of Bogomolnaia, Moulin, and Stong (2005) by showing that no strategyproof and efficient rule can guarantee that at least one approved project of each agent receives a positive amount of the resource. The proof reasons about 386 preference profiles and was obtained using a computer-aided method involving SAT solvers. I will also discuss a number of open problems.