Planning as Satisfiability is one of the most well-known and effective techniques for classical planning: satplan has been the winning system in the deterministic track for optimal planners in the 4th International Planning Competition (IPC) and a cowinner in the 5th IPC. Given a planning problem Π and a makespan n, the approach based on satisfiability (a.k.a. SAT-based) simply works by (i) constructing a SAT formula Πn and (ii) checking Πn for satisfiability: if there is a model for Πn then we have found a plan, otherwise n is increased. The approach guarantees that the makespan is optimal, i.e. minimum. In this article we extend the Planning as Satisfiability approach in order to handle preferences and satplan in order to solve problems with simple preferences. This allows, e.g. to take into consideration ‘plan quality’issues other than makespan, like number of actions and ‘soft’ goals. The basic idea is to explore the search space of possible plans in accordance wit...