As robots move out of the laboratory and into an unstructured world, they are asked to address more and more complicated tasks. Rather grip an object, they are asked to pack a box; rather than move to a location, they are asked to clean a room. Most robot demonstrations require a human to work out the details of a viable plan to accomplish its task, allowing designers the opportunity to carefully engineer solutions to a sequence of well-specified and narrowly scoped tasks. Specifying these details is difficult in unstructured domains, and alternative approaches that automate this specification often rely heavily on approximations that prevent us from understanding when the system will fail. In this talk I describe algorithms for planning in domains with many objects and complex constraints, and show how these algorithms allow us plan efficiently while also making strong theoretical guarantees. Along the way I will present a theoretical framework for modelling such systems, a simple way of parameterizing problems that is both verifiable and empirically derivable, and a strategy for incorporating abstraction in a way that preserves our theoretical guarantees.