Using an SMT solver for interactive requirements prioritization

The prioritization of requirements is a crucial activity in the early phases of the software development process. It consists of finding an order relation among requirements, considering several requirements characteristics, such as stakeholder preferences, technical constraints, implementation costs and user perceived value. We propose an interactive approach to the problem of prioritization based on Satisfiability Modulo Theory (SMT) techniques and pairwise comparisons. Our approach resorts to interactive knowledge acquisition whenever the relative priority among requirements cannot be determined based on the available information. Synthesis of the final ranking is obtained via SMT constraint solving. The approach has been evaluated on a set of require- ments from a real healthcare project. Results show that it overcomes other interactive state-of-the-art prioritization approaches in terms of effectiveness, efficiency and robust- ness to decision maker errors.